top

  Info

  • Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.

Biblioteca

MARC Lista (tabellare)
The inverse method : parametric verification of real-time embedded systems / / Etienne André, Romain Soulat
The inverse method : parametric verification of real-time embedded systems / / Etienne André, Romain Soulat
Autore André Etienne
Edizione [1st edition]
Pubbl/distr/stampa London, England ; ; Hoboken, New Jersey : , : iSTE : , : Wiley, , 2013
Descrizione fisica 1 online resource (170 p.)
Disciplina 004.16
Collana Focus Series in Computer Engineering and IT
Soggetto topico Embedded computer systems
Real-time data processing
Soggetto genere / forma Electronic books.
ISBN 1-118-56935-0
1-299-24214-6
1-118-56940-7
1-118-56978-4
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Blank Page; Title Page; Contents; PREFACE; ACKNOWLEDGEMENTS; INTRODUCTION; I.1. Motivation; I.1.1. An example of asynchronous circuit; I.2. The good parameters problem; I.3. Content and organization of the book; I.3.1. Content; I.3.2. Organization of the book; I.3.3. Acknowledgments; CHAPTER 1. PARAMETRIC TIMED AUTOMATA; 1.1. Constraints on clocks and parameters; 1.1.1. Clocks; 1.1.2. Parameters; 1.1.3. Constraints; 1.2. Labeled transition systems; 1.3. Timed automata; 1.3.1. Syntax; 1.3.2. Semantics; 1.4. Parametric timed automata; 1.4.1. Syntax; 1.4.2. Semantics; 1.5. Related work
1.5.1. Representation of time1.5.2. Timed automata; 1.5.3. Time Petri nets; 1.5.4. Hybrid systems; CHAPTER 2. THE INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA; 2.1. The inverse problem; 2.1.1. A motivating example; 2.1.2. The problem; 2.2. The inverse method algorithm; 2.2.1. Principle; 2.2.2. A toy example; 2.2.3. Remarks on the algorithm; 2.2.4. Results; 2.2.5. Discussion; 2.3. Variants of the inverse method; 2.3.1. Algorithm with state inclusion in the fixpoint; 2.3.2. Algorithm with union of the constraints; 2.3.3. Algorithm with simple return
2.3.4. Combination: inclusion in fixpoint and union2.3.5. Combination: inclusion in fixpoint and direct return; 2.3.6. Summary of the algorithms; 2.4. Related work; 2.4.1. History of the inverse method; 2.4.2. Time-abstract bisimulation; 2.4.3. Formal techniques of verification; 2.4.4. Problems related to the inverse problem; 2.4.5. Parameter synthesis for parametric timed automata; CHAPTER 3. THE INVERSE METHOD IN PRACTICE: APPLICATION TO CASE STUDIES; 3.1. IMITATOR; 3.1.1. History; 3.1.2. Architecture and features; 3.2. Flip-flop; 3.3. SR-Latch; 3.3.1. Parameter synthesis; 3.4. AND-OR
3.5. IEEE 1394 Root Contention Protocol3.5.1. Description of the model; 3.5.2. Synthesis of constraints; 3.6. Bounded Retransmission Protocol; 3.7. CSMA/CD protocol; 3.8. The SPSMALL memory; 3.8.1. Description; 3.8.2. A short history; 3.8.3. Manually abstracted model; 3.8.4. Automatically generated model; 3.9. Networked automation system; 3.9.1. Description of the model; 3.9.2. Definition of a zone of good behavior; 3.9.3. Comparison with other methods; 3.10. Tools related to IMITATOR; CHAPTER 4. BEHAVIORAL CARTOGRAPHY OF TIMED AUTOMATA; 4.1. The behavioral cartography algorithm
4.2. Properties4.2.1. Acyclic parametric timed automata; 4.2.2. General case; 4.3. Case studies; 4.3.1. Implementation; 4.3.2. SR latch; 4.3.3. Flip-flop; 4.3.4. The root contention protocol; 4.3.5. SPSMALL memory; 4.4. Related work; CHAPTER 5. PARAMETER SYNTHESIS FOR HYBRID AUTOMATA; 5.1. Hybrid automata with parameters; 5.1.1. Basic definitions; 5.1.2. Symbolic semantics of linear hybrid automata; 5.2. Algorithms for hybrid automata; 5.2.1. The inverse method for hybrid automata; 5.2.2. Behavioral cartography of hybrid automata; 5.2.3. Enhancement of the method for affine dynamics
5.3. Implementation
Record Nr. UNINA-9910141598503321
André Etienne  
London, England ; ; Hoboken, New Jersey : , : iSTE : , : Wiley, , 2013
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
The inverse method : parametric verification of real-time embedded systems / / Etienne André, Romain Soulat
The inverse method : parametric verification of real-time embedded systems / / Etienne André, Romain Soulat
Autore André Etienne
Edizione [1st edition]
Pubbl/distr/stampa London, England ; ; Hoboken, New Jersey : , : iSTE : , : Wiley, , 2013
Descrizione fisica 1 online resource (170 p.)
Disciplina 004.16
Collana Focus Series in Computer Engineering and IT
Soggetto topico Embedded computer systems
Real-time data processing
ISBN 1-118-56935-0
1-299-24214-6
1-118-56940-7
1-118-56978-4
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Blank Page; Title Page; Contents; PREFACE; ACKNOWLEDGEMENTS; INTRODUCTION; I.1. Motivation; I.1.1. An example of asynchronous circuit; I.2. The good parameters problem; I.3. Content and organization of the book; I.3.1. Content; I.3.2. Organization of the book; I.3.3. Acknowledgments; CHAPTER 1. PARAMETRIC TIMED AUTOMATA; 1.1. Constraints on clocks and parameters; 1.1.1. Clocks; 1.1.2. Parameters; 1.1.3. Constraints; 1.2. Labeled transition systems; 1.3. Timed automata; 1.3.1. Syntax; 1.3.2. Semantics; 1.4. Parametric timed automata; 1.4.1. Syntax; 1.4.2. Semantics; 1.5. Related work
1.5.1. Representation of time1.5.2. Timed automata; 1.5.3. Time Petri nets; 1.5.4. Hybrid systems; CHAPTER 2. THE INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA; 2.1. The inverse problem; 2.1.1. A motivating example; 2.1.2. The problem; 2.2. The inverse method algorithm; 2.2.1. Principle; 2.2.2. A toy example; 2.2.3. Remarks on the algorithm; 2.2.4. Results; 2.2.5. Discussion; 2.3. Variants of the inverse method; 2.3.1. Algorithm with state inclusion in the fixpoint; 2.3.2. Algorithm with union of the constraints; 2.3.3. Algorithm with simple return
2.3.4. Combination: inclusion in fixpoint and union2.3.5. Combination: inclusion in fixpoint and direct return; 2.3.6. Summary of the algorithms; 2.4. Related work; 2.4.1. History of the inverse method; 2.4.2. Time-abstract bisimulation; 2.4.3. Formal techniques of verification; 2.4.4. Problems related to the inverse problem; 2.4.5. Parameter synthesis for parametric timed automata; CHAPTER 3. THE INVERSE METHOD IN PRACTICE: APPLICATION TO CASE STUDIES; 3.1. IMITATOR; 3.1.1. History; 3.1.2. Architecture and features; 3.2. Flip-flop; 3.3. SR-Latch; 3.3.1. Parameter synthesis; 3.4. AND-OR
3.5. IEEE 1394 Root Contention Protocol3.5.1. Description of the model; 3.5.2. Synthesis of constraints; 3.6. Bounded Retransmission Protocol; 3.7. CSMA/CD protocol; 3.8. The SPSMALL memory; 3.8.1. Description; 3.8.2. A short history; 3.8.3. Manually abstracted model; 3.8.4. Automatically generated model; 3.9. Networked automation system; 3.9.1. Description of the model; 3.9.2. Definition of a zone of good behavior; 3.9.3. Comparison with other methods; 3.10. Tools related to IMITATOR; CHAPTER 4. BEHAVIORAL CARTOGRAPHY OF TIMED AUTOMATA; 4.1. The behavioral cartography algorithm
4.2. Properties4.2.1. Acyclic parametric timed automata; 4.2.2. General case; 4.3. Case studies; 4.3.1. Implementation; 4.3.2. SR latch; 4.3.3. Flip-flop; 4.3.4. The root contention protocol; 4.3.5. SPSMALL memory; 4.4. Related work; CHAPTER 5. PARAMETER SYNTHESIS FOR HYBRID AUTOMATA; 5.1. Hybrid automata with parameters; 5.1.1. Basic definitions; 5.1.2. Symbolic semantics of linear hybrid automata; 5.2. Algorithms for hybrid automata; 5.2.1. The inverse method for hybrid automata; 5.2.2. Behavioral cartography of hybrid automata; 5.2.3. Enhancement of the method for affine dynamics
5.3. Implementation
Record Nr. UNINA-9910831033803321
André Etienne  
London, England ; ; Hoboken, New Jersey : , : iSTE : , : Wiley, , 2013
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui