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.
Communicating embedded systems [[electronic resource] ] : software and design : formal methods / / edited by Claude Jard, Olivier H. Roux
| Communicating embedded systems [[electronic resource] ] : software and design : formal methods / / edited by Claude Jard, Olivier H. Roux |
| Edizione | [1st edition] |
| Pubbl/distr/stampa | London, : ISTE |
| Descrizione fisica | 1 online resource (275 p.) |
| Disciplina | 621.39/2 |
| Altri autori (Persone) |
JardClaude
RouxOlivier H |
| Collana | ISTE |
| Soggetto topico |
Embedded computer systems - Programming
Embedded computer systems - Design and construction Computer software - Development Formal methods (Computer science) |
| ISBN |
1-118-55818-9
1-118-60009-6 1-118-60012-6 1-299-18745-5 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Cover; Communicating Embedded Systems; Title Page; Copyright Page; Table of Contents; Preface; Chapter 1. Models for Real-Time Embedded Systems; 1.1. Introduction; 1.1.1. Model-checking and control problems; 1.1.2. Timed models; 1.2. Notations, languages and timed transition systems; 1.3. Timed models; 1.3.1. Timed Automata; 1.3.2. Time Petri nets; 1.3.2.1. T-time Petri nets; 1.3.2.2. Timed-arc petri nets; 1.3.3. Compared expressiveness of several classes of timed models; 1.3.3.1. Bisimulation and expressiveness of timed models; 1.3.3.2. Compared expressiveness of different classes of TPN
1.3.3.3. Compared expressiveness of TA, TPN, and TAPN1.4. Models with stopwatches; 1.4.1. Formal models for scheduling aspects; 1.4.1.1. Automata and scheduling; 1.4.1.2. Time Petri nets and scheduling; 1.4.2. Stopwatch automata; 1.4.3. Scheduling time Petri nets; 1.4.4. Decidability results for stopwatch models; 1.5. Conclusion; 1.6. Bibliography; Chapter 2. Timed Model-Checking; 2.1. Introduction; 2.2. Timed models; 2.2.1. Timed transition system; 2.2.2. Timed automata; 2.2.3. Other models; 2.3. Timed logics; 2.3.1. Temporal logics CTL and LTL; 2.3.2. Timed extensions; 2.3.2.1. Timed CTL 2.3.2.2. Timed LTL2.4. Timed model-checking; 2.4.1. Model-checking LTL and CTL (untimed case); 2.4.2. Region automaton; 2.4.3. Model-checking TCTL; 2.4.4. Model-checking MTL; 2.4.5. Efficient model-checking; 2.4.6. Model-checking in practice; 2.5. Conclusion; 2.6. Bibliography; Chapter 3. Control of Timed Systems; 3.1. Introduction; 3.1.1. Verification of timed systems; 3.1.2. The controller synthesis problem; 3.1.3. From control to game; 3.1.4. Game objectives; 3.1.5. Varieties of untimed games; 3.2. Timed games; 3.2.1. Timed game automata; 3.2.2. Strategies and course of the game 3.2.2.1. The course of a timed game3.2.2.2. Strategies; 3.3. Computation of winning states and strategies; 3.3.1. Controllable predecessors; 3.3.2. Symbolic operators; 3.3.3. Symbolic computation of winning states; 3.3.4. Synthesis of winning strategies; 3.4. Zeno strategies; 3.5. Implementability; 3.5.1. Hybrid automata; 3.5.2. On the existence of non-implementable continuous controllers; 3.5.3. Recent results and open problems; 3.6. Specification of control objectives; 3.7. Optimal control; 3.7.1. TA with costs; 3.7.2. Optimal cost in timed games; 3.7.3. Computation of the optimal cost 3.7.4. Recent results and open problems3.8. Efficient algorithms for controller synthesis; 3.8.1. On-the-fly algorithms; 3.8.2. Recent results and open problems; 3.9. Partial observation; 3.10. Changing game rules...; 3.11. Bibliography; Chapter 4. Fault Diagnosis of Timed Systems; 4.1. Introduction; 4.2. Notations; 4.2.1. Timed words and timed languages; 4.2.2. Timed automata; 4.2.3. Region graph of a TA; 4.2.4. Product of TA; 4.2.5. Timed automata with faults; 4.3. Fault diagnosis problems; 4.3.1. Diagnoser; 4.3.2. The problems; 4.3.3. Necessary and sufficient condition for diagnosability 4.4. Fault diagnosis for discrete event systems |
| Record Nr. | UNINA-9910138854403321 |
| London, : ISTE | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Communicating embedded systems : software and design : formal methods / / edited by Claude Jard, Olivier H. Roux
| Communicating embedded systems : software and design : formal methods / / edited by Claude Jard, Olivier H. Roux |
| Edizione | [1st edition] |
| Pubbl/distr/stampa | London, : ISTE |
| Descrizione fisica | 1 online resource (275 p.) |
| Disciplina | 621.39/2 |
| Altri autori (Persone) |
JardClaude
RouxOlivier H |
| Collana | ISTE |
| Soggetto topico |
Embedded computer systems - Programming
Embedded computer systems - Design and construction Computer software - Development Formal methods (Computer science) |
| ISBN |
1-118-55818-9
1-118-60009-6 1-118-60012-6 1-299-18745-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Cover; Communicating Embedded Systems; Title Page; Copyright Page; Table of Contents; Preface; Chapter 1. Models for Real-Time Embedded Systems; 1.1. Introduction; 1.1.1. Model-checking and control problems; 1.1.2. Timed models; 1.2. Notations, languages and timed transition systems; 1.3. Timed models; 1.3.1. Timed Automata; 1.3.2. Time Petri nets; 1.3.2.1. T-time Petri nets; 1.3.2.2. Timed-arc petri nets; 1.3.3. Compared expressiveness of several classes of timed models; 1.3.3.1. Bisimulation and expressiveness of timed models; 1.3.3.2. Compared expressiveness of different classes of TPN
1.3.3.3. Compared expressiveness of TA, TPN, and TAPN1.4. Models with stopwatches; 1.4.1. Formal models for scheduling aspects; 1.4.1.1. Automata and scheduling; 1.4.1.2. Time Petri nets and scheduling; 1.4.2. Stopwatch automata; 1.4.3. Scheduling time Petri nets; 1.4.4. Decidability results for stopwatch models; 1.5. Conclusion; 1.6. Bibliography; Chapter 2. Timed Model-Checking; 2.1. Introduction; 2.2. Timed models; 2.2.1. Timed transition system; 2.2.2. Timed automata; 2.2.3. Other models; 2.3. Timed logics; 2.3.1. Temporal logics CTL and LTL; 2.3.2. Timed extensions; 2.3.2.1. Timed CTL 2.3.2.2. Timed LTL2.4. Timed model-checking; 2.4.1. Model-checking LTL and CTL (untimed case); 2.4.2. Region automaton; 2.4.3. Model-checking TCTL; 2.4.4. Model-checking MTL; 2.4.5. Efficient model-checking; 2.4.6. Model-checking in practice; 2.5. Conclusion; 2.6. Bibliography; Chapter 3. Control of Timed Systems; 3.1. Introduction; 3.1.1. Verification of timed systems; 3.1.2. The controller synthesis problem; 3.1.3. From control to game; 3.1.4. Game objectives; 3.1.5. Varieties of untimed games; 3.2. Timed games; 3.2.1. Timed game automata; 3.2.2. Strategies and course of the game 3.2.2.1. The course of a timed game3.2.2.2. Strategies; 3.3. Computation of winning states and strategies; 3.3.1. Controllable predecessors; 3.3.2. Symbolic operators; 3.3.3. Symbolic computation of winning states; 3.3.4. Synthesis of winning strategies; 3.4. Zeno strategies; 3.5. Implementability; 3.5.1. Hybrid automata; 3.5.2. On the existence of non-implementable continuous controllers; 3.5.3. Recent results and open problems; 3.6. Specification of control objectives; 3.7. Optimal control; 3.7.1. TA with costs; 3.7.2. Optimal cost in timed games; 3.7.3. Computation of the optimal cost 3.7.4. Recent results and open problems3.8. Efficient algorithms for controller synthesis; 3.8.1. On-the-fly algorithms; 3.8.2. Recent results and open problems; 3.9. Partial observation; 3.10. Changing game rules...; 3.11. Bibliography; Chapter 4. Fault Diagnosis of Timed Systems; 4.1. Introduction; 4.2. Notations; 4.2.1. Timed words and timed languages; 4.2.2. Timed automata; 4.2.3. Region graph of a TA; 4.2.4. Product of TA; 4.2.5. Timed automata with faults; 4.3. Fault diagnosis problems; 4.3.1. Diagnoser; 4.3.2. The problems; 4.3.3. Necessary and sufficient condition for diagnosability 4.4. Fault diagnosis for discrete event systems |
| Record Nr. | UNINA-9910820091003321 |
| London, : ISTE | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal Modeling and Analysis of Timed Systems [[electronic resource] ] : 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008, Proceedings / / edited by Franck Cassez, Claude Jard
| Formal Modeling and Analysis of Timed Systems [[electronic resource] ] : 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008, Proceedings / / edited by Franck Cassez, Claude Jard |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 |
| Descrizione fisica | 1 online resource (X, 295 p.) |
| Disciplina | 004.33 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer programming
Computer science Software engineering Compilers (Computer programs) Programming Techniques Theory of Computation Software Engineering Computer Science Logic and Foundations of Programming Models of Computation Compilers and Interpreters |
| ISBN | 3-540-85778-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Some Recent Results in Metric Temporal Logic -- Composing Web Services in an Open World: Issues of Quality of Service -- Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets -- Session 1. Extensions of Timed Automata and Semantics -- Infinite Runs in Weighted Timed Automata with Energy Constraints -- Concavely-Priced Timed Automata -- Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets -- Timed Automata with Integer Resets: Language Inclusion and Expressiveness -- Session 2. Timed Games and Logic -- Complexity of Metric Temporal Logics with Counting and the Pnueli Modalities -- MTL with Bounded Variability: Decidability and Complexity -- Timed Parity Games: Complexity and Robustness -- On Scheduling Policies for Streams of Structured Jobs -- Session 3. Case Studies -- A Framework for Distributing Real-Time Functions -- Formal Modeling and Scheduling of Datapaths of Digital Document Printers -- Session 4. Model-Checking of Probabilistic Systems -- A Uniformization-Based Algorithm for Model Checking the CSL Until Operator on Labeled Queueing Networks -- Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains -- Session 5. Verification and Test -- Convergence Verification: From Shared Memory to Partially Synchronous Systems -- Compositional Abstraction in Real-Time Model Checking -- On Conformance Testing for Timed Systems -- Session 6. Time Petri Nets -- Relevant Timed Schedules / Clock Valuations for Constructing Time Petri Net Reachability Graphs -- Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph. |
| Record Nr. | UNISA-996465918303316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal Modeling and Analysis of Timed Systems : 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008, Proceedings / / edited by Franck Cassez, Claude Jard
| Formal Modeling and Analysis of Timed Systems : 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008, Proceedings / / edited by Franck Cassez, Claude Jard |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 |
| Descrizione fisica | 1 online resource (X, 295 p.) |
| Disciplina | 004.33 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer programming
Computer science Software engineering Compilers (Computer programs) Programming Techniques Theory of Computation Software Engineering Computer Science Logic and Foundations of Programming Models of Computation Compilers and Interpreters |
| ISBN | 3-540-85778-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Some Recent Results in Metric Temporal Logic -- Composing Web Services in an Open World: Issues of Quality of Service -- Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets -- Session 1. Extensions of Timed Automata and Semantics -- Infinite Runs in Weighted Timed Automata with Energy Constraints -- Concavely-Priced Timed Automata -- Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets -- Timed Automata with Integer Resets: Language Inclusion and Expressiveness -- Session 2. Timed Games and Logic -- Complexity of Metric Temporal Logics with Counting and the Pnueli Modalities -- MTL with Bounded Variability: Decidability and Complexity -- Timed Parity Games: Complexity and Robustness -- On Scheduling Policies for Streams of Structured Jobs -- Session 3. Case Studies -- A Framework for Distributing Real-Time Functions -- Formal Modeling and Scheduling of Datapaths of Digital Document Printers -- Session 4. Model-Checking of Probabilistic Systems -- A Uniformization-Based Algorithm for Model Checking the CSL Until Operator on Labeled Queueing Networks -- Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains -- Session 5. Verification and Test -- Convergence Verification: From Shared Memory to Partially Synchronous Systems -- Compositional Abstraction in Real-Time Model Checking -- On Conformance Testing for Timed Systems -- Session 6. Time Petri Nets -- Relevant Timed Schedules / Clock Valuations for Constructing Time Petri Net Reachability Graphs -- Parametric Model-Checking of Time Petri Nets with Stopwatches Using the State-Class Graph. |
| Record Nr. | UNINA-9910484241503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Modeling and Verification of Parallel Processes [[electronic resource] ] : 4th Summer School, MOVEP 2000, Nantes, France, June 19-23, 2000. Revised Tutorial Lectures / / edited by Franck Cassez, Claude Jard, Brigitte Rozoy, Mark D. Ryan
| Modeling and Verification of Parallel Processes [[electronic resource] ] : 4th Summer School, MOVEP 2000, Nantes, France, June 19-23, 2000. Revised Tutorial Lectures / / edited by Franck Cassez, Claude Jard, Brigitte Rozoy, Mark D. Ryan |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (X, 234 p.) |
| Disciplina | 004/.358 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computers Software Engineering Theory of Computation |
| ISBN | 3-540-45510-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Tutorials and Papers -- Model Checking: A Tutorial Overview -- Theorem Proving for Verification -- Composition and Abstraction -- UPPAAL - Now, Next, and Future -- HMSCs as Partial Specifications...with PNs as Completions -- Industrial Applications of Model Checking -- Formal Methods in Practice: The Missing Links. A Perspective from the Security Area -- Annotated Bibliographies -- Verification of Systems with an Infinite State Space -- Testing Transition Systems: An Annotated Bibliography -- Fault Model-Driven Test Derivation from Finite State Models: Annotated Bibliography -- Mobile Processes: A Commented Bibliography. |
| Record Nr. | UNISA-996465885303316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Modeling and Verification of Parallel Processes : 4th Summer School, MOVEP 2000, Nantes, France, June 19-23, 2000. Revised Tutorial Lectures / / edited by Franck Cassez, Claude Jard, Brigitte Rozoy, Mark D. Ryan
| Modeling and Verification of Parallel Processes : 4th Summer School, MOVEP 2000, Nantes, France, June 19-23, 2000. Revised Tutorial Lectures / / edited by Franck Cassez, Claude Jard, Brigitte Rozoy, Mark D. Ryan |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (X, 234 p.) |
| Disciplina | 004/.358 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computers Software Engineering Theory of Computation |
| ISBN | 3-540-45510-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Tutorials and Papers -- Model Checking: A Tutorial Overview -- Theorem Proving for Verification -- Composition and Abstraction -- UPPAAL - Now, Next, and Future -- HMSCs as Partial Specifications...with PNs as Completions -- Industrial Applications of Model Checking -- Formal Methods in Practice: The Missing Links. A Perspective from the Security Area -- Annotated Bibliographies -- Verification of Systems with an Infinite State Space -- Testing Transition Systems: An Annotated Bibliography -- Fault Model-Driven Test Derivation from Finite State Models: Annotated Bibliography -- Mobile Processes: A Commented Bibliography. |
| Record Nr. | UNINA-9910143601403321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||