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.
Dependable Software Engineering: Theories, Tools, and Applications [[electronic resource] ] : First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings / / edited by Xuandong Li, Zhiming Liu, Wang Yi
| Dependable Software Engineering: Theories, Tools, and Applications [[electronic resource] ] : First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings / / edited by Xuandong Li, Zhiming Liu, Wang Yi |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XIX, 317 p. 86 illus.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer logic Computer simulation Mathematical logic Software Engineering Logics and Meanings of Programs Simulation and Modeling Mathematical Logic and Formal Languages |
| ISBN | 3-319-25942-3 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Invited Talks -- Criticality-Cognizant Modeling and Analysis of Mixed-Criticality Systems (Extended Abstract) -- Wise Computing (Abstract of Invited Lecture) -- The Myth of Linearization Points -- Contents -- Probabilistic Systems -- Fault Trees on a Diet -- 1 Introduction -- 2 Dynamic Fault Trees -- 3 Rewrite Rules for Dynamic Fault Trees -- 4 Rewriting DFTs via Graph Transformation -- 5 Experiments -- 6 Conclusions and Future Work -- Cost vs. Time in Stochastic Games and Markov Automata -- 1 Introduction -- 2 Foundations -- 3 Transformation of Stochastic Games -- 4 Case Studies and Experimental Results -- 5 Conclusion -- References -- A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking -- 1 Introduction -- 2 Probabilistic Model Checking -- 2.1 Markov Decision Processes -- 2.2 PCTL Model Checking -- 2.3 BDD-Based Probabilistic Symbolic Model Checking -- 2.4 BDD Packages -- 3 Experimental Results -- 4 Conclusion -- References -- Hybrid and Cyber-Physical Systems -- Refinement and Proof Based Development of Systems Characterized by Continuous Functions -- 1 Introduction -- 2 Discretization of Continuous Functions -- 3 The Event-B Method -- 4 Refinement Strategy -- 4.1 The Illustrating System -- 4.2 Continuous Controller -- 4.3 Discrete Controller -- 4.4 Top-Down Refinement -- 4.5 About Modeling of Time -- 5 A Formal Development of a Discrete Controller with Event-B -- 5.1 Abstract Machine: The Top-Level Specification -- 5.2 The First Refinement: Introducing Continuous Functions -- 5.3 The Second Refinement: Introducing Discrete Representation -- 5.4 Proofs Statistics -- 6 Related Works and Applications -- 7 Conclusion -- References -- Synthesizing Controllers for Multi-lane Traffic Maneuvers -- 1 Introduction -- 2 Car Traffic Modeling -- 2.1 The Multi-lane Highway.
2.2 A Hybrid Model of a Car -- 2.3 Highway Traffic with Lane Change -- 3 Controller Synthesis for Multi-lane Traffic Maneuvers -- 3.1 Overview of Controller Synthesis -- 3.2 A Simple Algorithm for Lane Change -- 3.3 Interleaving Semantics or Synchronous Models? -- 3.4 Lane Change Algorithm Allowing for Parallel Transitions -- 3.5 Using a Helper Car -- 4 Conclusion -- References -- Extending Hybrid CSP with Probability and Stochasticity -- 1 Introduction -- 2 Background and Notations -- 3 Stochastic HCSP -- 3.1 A Running Example -- 4 Operational Semantics -- 4.1 Operational Semantics -- 5 Assertions and Specifications -- 5.1 Assertion Language -- 5.2 Specifications -- 6 Proof System -- 7 Conclusion -- References -- Testing, Simulation and Inference -- Towards Verified Faithful Simulation -- 1 Introduction -- 2 Related Work -- 3 Background -- 3.1 Coq -- 3.2 Compert-C -- 3.3 SimSoC -- 4 Verified Simulation -- 4.1 Constructing the Formal Model -- 4.2 Proof Structure -- 4.3 Projection -- 4.4 Lemmas Library -- 4.5 Inversion -- 4.6 Instruction Proofs -- 5 Conclusion -- References -- Cardinality of UDP Transmission Outcomes -- 1 Introduction -- 2 Background -- 3 Formal Analysis of Unreliable UDP Behavior -- 3.1 Unreliable UDP Transmissions -- 3.2 Cardinality of Unreliable UDP Transmissions -- 4 Generating UDP Transmission Outcomes -- 5 Experimental Results -- 6 Related Work -- 7 Conclusion -- References -- Inferring Software Behavioral Models with MapReduce -- 1 Introduction -- 2 Approach Overview -- 2.1 MapReduce -- 2.2 Behavioral Model Inference -- 2.3 Our Approach -- 3 Formal Definitions -- 4 Distributed Trace Slicing with MapReduce -- 4.1 Data Encoding -- 4.2 Mapper -- 4.3 Reducer -- 5 Distributed Model Synthesis with MapReduce -- 5.1 Data Encoding -- 5.2 Mapper and Reducer -- 6 Experimental Evaluation -- 7 Related Works -- 8 Conclusion -- References. Bisimulation and Correctness -- An Application of Temporal Projection to Interleaving Concurrency -- 1 Introduction -- 2 Propositional Interval Temporal Logic -- 3 Temporal Projection -- 4 Formalisation of Imperative Concurrent Programs -- 4.1 Formalising Interleaving without Projection -- 4.2 Comparison of State Projection with Time-Step Projection -- 5 Related Work -- References -- A High-Level Model for an Assembly Language Attacker by Means of Reflection -- 1 Introduction -- 2 Security Overview -- 2.1 PMA and the Assembly Language Attacker -- 2.2 Contextual Equivalence -- 2.3 The High-Level Attacker Model La -- 3 A Bisimulation over the High-Level Attacker -- 3.1 The Source Language MiniML -- 3.2 The High-Level Attacker Model MiniMLa -- 3.3 MiniML+: Interoperation Between MiniMLa and MiniML -- 3.4 Ba: A Bisimulation over the MiniMLa Attacker -- 4 A Bisimulation over the Assembly Language Attacker -- 4.1 A Trace Semantics for the Assembly Language Attacker -- 4.2 Bl: A Bisimulation over the Assembly Language Attacker -- 5 Full Abstraction -- 6 Related Work -- 7 Conclusions -- References -- Design and Implementation -- Improving Design Decomposition -- 1 Introduction -- 2 A Relational Model of Software Systems -- 3 Subsystem Decomposition -- 4 Case Studies -- 5 Related Work -- 6 Summary -- References -- From Requirements Engineering to Safety Assurance: Refinement Approach -- 1 Introduction -- 2 Modelling and Verification of Safety-Critical Systems in Event-B -- 3 From Event-B Models to Safety Cases -- 4 Case Study: A Steam Boiler System -- 5 Integrated Automated Tool Support -- 6 Related Work and Conclusions -- References -- Pareto Optimal Scheduling of Synchronous Data Flow Graphs via Parallel Methods -- 1 Introduction and Related Work -- 2 System Model and Problem Formulation -- 3 Pareto Optimal Scheduling and Mapping -- 4 Experiments. 5 Conclusion -- References -- Symbolic Execution and Invariants -- PathWalker: A Dynamic Symbolic Execution Tool Based on LLVM Byte Code Instrumentation -- 1 Introduction -- 1.1 Background -- 1.2 Overview -- 1.3 Contributions -- 1.4 Structure of the Paper -- 2 Example -- 3 Our Approach -- 3.1 Concolic Execution -- 3.2 Splitting Complex Type Variable -- 3.3 Generation of Test Driver -- 3.4 Program Instrumentation Based on LLVM Byte Code -- 4 Implementation and Evaluation -- 4.1 Implementation -- 4.2 Evaluation -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Generating Specifications for Recursive Methods by Abstracting Program States -- 1 Introduction -- 2 Methodology -- 3 Application Scenarios -- 4 Background -- 4.1 Program Logic -- 4.2 Integrating Abstraction -- 5 Generation of Method Contracts -- 5.1 Example -- 5.2 Gathering Partial Method Contracts -- 5.3 Dealing with Other Method Calls, Mutual Recursion -- 6 Experimental Evaluation -- 7 Related Work -- 8 Conclusion and Future Work -- References -- Assertion-Directed Precondition Synthesis for Loops over Data Structures -- 1 Introduction -- 2 Preliminary -- 2.1 Scope Logic -- 2.2 Weakest-Precondition Calculus in Scope Logic -- 3 Motivating Example -- 4 Design -- 4.1 Information Extractor -- 4.2 Pre-processor -- 4.3 Pre-condition Generator -- 4.4 Checking Precondition Candidates -- 5 Implementation and Application -- 6 Limitations -- 7 Related Work -- 8 Conclusion -- References -- Verification and Case Studies -- Automatic Fault Localization for BIP -- 1 Introduction -- 2 The BIP Language -- 3 Overview of the Algorithm -- 4 Fault Localization Algorithm for BIP -- 5 Experimental Evaluation -- 6 Conclusion -- References -- Formal Verification of the Pastry Protocol Using TLA+ -- 1 Introduction -- 1.1 The Pastry Protocol -- 1.2 The Methodology. 2 Modelling the Concurrent Join Protocol of Pastry -- 2.1 Static Model -- Leaf Set. -- Messages. -- Statuses. -- 2.2 Dynamic Model -- 2.3 The Correctness Properties -- 3 Theorem Proving -- 3.1 Inductive Proof of Invariant HalfNeighbor -- 3.2 Proof of NeighborClosest -- Induction Invariant. -- Proof Sketch of the Invariant IRN. -- 4 Conclusion, Related Work and Future Work -- References -- Formal Modelling and Verification of IEC61499Function Blocks with Abstract State Machinesand SMV - Execution Semantics -- 1 Introduction -- 2 Related Facts -- 2.1 Function Blocks -- 2.2 Abstract State Machines -- 2.3 Formal Modeling of IEC 61499 and Cross-Platform Portability -- 3 Functional Structure of Operational Model -- 4 Modular formalism for FB operational semantics - Synchronous Execution -- 4.1 Definition of Scheme for the Model -- 4.2 Definition of Dynamics of the Model -- 4.3 Model of the Dispatcher for Synchronous Execution Model -- 5 Model of the Dispatcher in SMV -- 6 Verification Results -- 7 Conclusion and Future Work -- References -- Erratum to: Pareto Optimal Scheduling of Synchronous Data Flow Graphs via Parallel Methods -- Erratum to: Formal Modelling and Verification of IEC61499 Function Blocks with Abstract State Machines and SMV - Execution Semantics -- Author Index. |
| Record Nr. | UNISA-996466445303316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Dependable Software Engineering: Theories, Tools, and Applications : First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings / / edited by Xuandong Li, Zhiming Liu, Wang Yi
| Dependable Software Engineering: Theories, Tools, and Applications : First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings / / edited by Xuandong Li, Zhiming Liu, Wang Yi |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XIX, 317 p. 86 illus.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer logic Computer simulation Mathematical logic Software Engineering Logics and Meanings of Programs Simulation and Modeling Mathematical Logic and Formal Languages |
| ISBN | 3-319-25942-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Invited Talks -- Criticality-Cognizant Modeling and Analysis of Mixed-Criticality Systems (Extended Abstract) -- Wise Computing (Abstract of Invited Lecture) -- The Myth of Linearization Points -- Contents -- Probabilistic Systems -- Fault Trees on a Diet -- 1 Introduction -- 2 Dynamic Fault Trees -- 3 Rewrite Rules for Dynamic Fault Trees -- 4 Rewriting DFTs via Graph Transformation -- 5 Experiments -- 6 Conclusions and Future Work -- Cost vs. Time in Stochastic Games and Markov Automata -- 1 Introduction -- 2 Foundations -- 3 Transformation of Stochastic Games -- 4 Case Studies and Experimental Results -- 5 Conclusion -- References -- A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking -- 1 Introduction -- 2 Probabilistic Model Checking -- 2.1 Markov Decision Processes -- 2.2 PCTL Model Checking -- 2.3 BDD-Based Probabilistic Symbolic Model Checking -- 2.4 BDD Packages -- 3 Experimental Results -- 4 Conclusion -- References -- Hybrid and Cyber-Physical Systems -- Refinement and Proof Based Development of Systems Characterized by Continuous Functions -- 1 Introduction -- 2 Discretization of Continuous Functions -- 3 The Event-B Method -- 4 Refinement Strategy -- 4.1 The Illustrating System -- 4.2 Continuous Controller -- 4.3 Discrete Controller -- 4.4 Top-Down Refinement -- 4.5 About Modeling of Time -- 5 A Formal Development of a Discrete Controller with Event-B -- 5.1 Abstract Machine: The Top-Level Specification -- 5.2 The First Refinement: Introducing Continuous Functions -- 5.3 The Second Refinement: Introducing Discrete Representation -- 5.4 Proofs Statistics -- 6 Related Works and Applications -- 7 Conclusion -- References -- Synthesizing Controllers for Multi-lane Traffic Maneuvers -- 1 Introduction -- 2 Car Traffic Modeling -- 2.1 The Multi-lane Highway.
2.2 A Hybrid Model of a Car -- 2.3 Highway Traffic with Lane Change -- 3 Controller Synthesis for Multi-lane Traffic Maneuvers -- 3.1 Overview of Controller Synthesis -- 3.2 A Simple Algorithm for Lane Change -- 3.3 Interleaving Semantics or Synchronous Models? -- 3.4 Lane Change Algorithm Allowing for Parallel Transitions -- 3.5 Using a Helper Car -- 4 Conclusion -- References -- Extending Hybrid CSP with Probability and Stochasticity -- 1 Introduction -- 2 Background and Notations -- 3 Stochastic HCSP -- 3.1 A Running Example -- 4 Operational Semantics -- 4.1 Operational Semantics -- 5 Assertions and Specifications -- 5.1 Assertion Language -- 5.2 Specifications -- 6 Proof System -- 7 Conclusion -- References -- Testing, Simulation and Inference -- Towards Verified Faithful Simulation -- 1 Introduction -- 2 Related Work -- 3 Background -- 3.1 Coq -- 3.2 Compert-C -- 3.3 SimSoC -- 4 Verified Simulation -- 4.1 Constructing the Formal Model -- 4.2 Proof Structure -- 4.3 Projection -- 4.4 Lemmas Library -- 4.5 Inversion -- 4.6 Instruction Proofs -- 5 Conclusion -- References -- Cardinality of UDP Transmission Outcomes -- 1 Introduction -- 2 Background -- 3 Formal Analysis of Unreliable UDP Behavior -- 3.1 Unreliable UDP Transmissions -- 3.2 Cardinality of Unreliable UDP Transmissions -- 4 Generating UDP Transmission Outcomes -- 5 Experimental Results -- 6 Related Work -- 7 Conclusion -- References -- Inferring Software Behavioral Models with MapReduce -- 1 Introduction -- 2 Approach Overview -- 2.1 MapReduce -- 2.2 Behavioral Model Inference -- 2.3 Our Approach -- 3 Formal Definitions -- 4 Distributed Trace Slicing with MapReduce -- 4.1 Data Encoding -- 4.2 Mapper -- 4.3 Reducer -- 5 Distributed Model Synthesis with MapReduce -- 5.1 Data Encoding -- 5.2 Mapper and Reducer -- 6 Experimental Evaluation -- 7 Related Works -- 8 Conclusion -- References. Bisimulation and Correctness -- An Application of Temporal Projection to Interleaving Concurrency -- 1 Introduction -- 2 Propositional Interval Temporal Logic -- 3 Temporal Projection -- 4 Formalisation of Imperative Concurrent Programs -- 4.1 Formalising Interleaving without Projection -- 4.2 Comparison of State Projection with Time-Step Projection -- 5 Related Work -- References -- A High-Level Model for an Assembly Language Attacker by Means of Reflection -- 1 Introduction -- 2 Security Overview -- 2.1 PMA and the Assembly Language Attacker -- 2.2 Contextual Equivalence -- 2.3 The High-Level Attacker Model La -- 3 A Bisimulation over the High-Level Attacker -- 3.1 The Source Language MiniML -- 3.2 The High-Level Attacker Model MiniMLa -- 3.3 MiniML+: Interoperation Between MiniMLa and MiniML -- 3.4 Ba: A Bisimulation over the MiniMLa Attacker -- 4 A Bisimulation over the Assembly Language Attacker -- 4.1 A Trace Semantics for the Assembly Language Attacker -- 4.2 Bl: A Bisimulation over the Assembly Language Attacker -- 5 Full Abstraction -- 6 Related Work -- 7 Conclusions -- References -- Design and Implementation -- Improving Design Decomposition -- 1 Introduction -- 2 A Relational Model of Software Systems -- 3 Subsystem Decomposition -- 4 Case Studies -- 5 Related Work -- 6 Summary -- References -- From Requirements Engineering to Safety Assurance: Refinement Approach -- 1 Introduction -- 2 Modelling and Verification of Safety-Critical Systems in Event-B -- 3 From Event-B Models to Safety Cases -- 4 Case Study: A Steam Boiler System -- 5 Integrated Automated Tool Support -- 6 Related Work and Conclusions -- References -- Pareto Optimal Scheduling of Synchronous Data Flow Graphs via Parallel Methods -- 1 Introduction and Related Work -- 2 System Model and Problem Formulation -- 3 Pareto Optimal Scheduling and Mapping -- 4 Experiments. 5 Conclusion -- References -- Symbolic Execution and Invariants -- PathWalker: A Dynamic Symbolic Execution Tool Based on LLVM Byte Code Instrumentation -- 1 Introduction -- 1.1 Background -- 1.2 Overview -- 1.3 Contributions -- 1.4 Structure of the Paper -- 2 Example -- 3 Our Approach -- 3.1 Concolic Execution -- 3.2 Splitting Complex Type Variable -- 3.3 Generation of Test Driver -- 3.4 Program Instrumentation Based on LLVM Byte Code -- 4 Implementation and Evaluation -- 4.1 Implementation -- 4.2 Evaluation -- 5 Related Work -- 6 Conclusion and Future Work -- References -- Generating Specifications for Recursive Methods by Abstracting Program States -- 1 Introduction -- 2 Methodology -- 3 Application Scenarios -- 4 Background -- 4.1 Program Logic -- 4.2 Integrating Abstraction -- 5 Generation of Method Contracts -- 5.1 Example -- 5.2 Gathering Partial Method Contracts -- 5.3 Dealing with Other Method Calls, Mutual Recursion -- 6 Experimental Evaluation -- 7 Related Work -- 8 Conclusion and Future Work -- References -- Assertion-Directed Precondition Synthesis for Loops over Data Structures -- 1 Introduction -- 2 Preliminary -- 2.1 Scope Logic -- 2.2 Weakest-Precondition Calculus in Scope Logic -- 3 Motivating Example -- 4 Design -- 4.1 Information Extractor -- 4.2 Pre-processor -- 4.3 Pre-condition Generator -- 4.4 Checking Precondition Candidates -- 5 Implementation and Application -- 6 Limitations -- 7 Related Work -- 8 Conclusion -- References -- Verification and Case Studies -- Automatic Fault Localization for BIP -- 1 Introduction -- 2 The BIP Language -- 3 Overview of the Algorithm -- 4 Fault Localization Algorithm for BIP -- 5 Experimental Evaluation -- 6 Conclusion -- References -- Formal Verification of the Pastry Protocol Using TLA+ -- 1 Introduction -- 1.1 The Pastry Protocol -- 1.2 The Methodology. 2 Modelling the Concurrent Join Protocol of Pastry -- 2.1 Static Model -- Leaf Set. -- Messages. -- Statuses. -- 2.2 Dynamic Model -- 2.3 The Correctness Properties -- 3 Theorem Proving -- 3.1 Inductive Proof of Invariant HalfNeighbor -- 3.2 Proof of NeighborClosest -- Induction Invariant. -- Proof Sketch of the Invariant IRN. -- 4 Conclusion, Related Work and Future Work -- References -- Formal Modelling and Verification of IEC61499Function Blocks with Abstract State Machinesand SMV - Execution Semantics -- 1 Introduction -- 2 Related Facts -- 2.1 Function Blocks -- 2.2 Abstract State Machines -- 2.3 Formal Modeling of IEC 61499 and Cross-Platform Portability -- 3 Functional Structure of Operational Model -- 4 Modular formalism for FB operational semantics - Synchronous Execution -- 4.1 Definition of Scheme for the Model -- 4.2 Definition of Dynamics of the Model -- 4.3 Model of the Dispatcher for Synchronous Execution Model -- 5 Model of the Dispatcher in SMV -- 6 Verification Results -- 7 Conclusion and Future Work -- References -- Erratum to: Pareto Optimal Scheduling of Synchronous Data Flow Graphs via Parallel Methods -- Erratum to: Formal Modelling and Verification of IEC61499 Function Blocks with Abstract State Machines and SMV - Execution Semantics -- Author Index. |
| Record Nr. | UNINA-9910484069303321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Formal Modeling and Analysis of Timed Systems [[electronic resource] ] : Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings / / edited by Paul Pettersson, Wang Yi
| Formal Modeling and Analysis of Timed Systems [[electronic resource] ] : Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings / / edited by Paul Pettersson, Wang Yi |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
| Descrizione fisica | 1 online resource (IX, 305 p.) |
| Disciplina | 005.1015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer logic
Software engineering Programming languages (Electronic computers) Special purpose computers Logics and Meanings of Programs Software Engineering Programming Languages, Compilers, Interpreters Special Purpose and Application-Based Systems |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk -- Modular Performance Analysis of Distributed Embedded Systems -- Logic and Specification -- Real Time Temporal Logic: Past, Present, Future -- Translating Timed I/O Automata Specifications for Theorem Proving in PVS -- Specification and Refinement of Soft Real-Time Requirements Using Sequence Diagrams -- Times Games and Synthesis -- On Optimal Timed Strategies -- Average Reward Timed Games -- Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness -- Invited Talk -- Verification of Parameterized Timed Systems -- Model Checking -- Model Checking the Time to Reach Agreement -- Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems -- A New Verification Procedure for Partially Clairvoyant Scheduling -- Invited Talk -- Timing Analysis and Simulation Tools for Real-Time Control -- Hybrid Systems -- Automatic Rectangular Refinement of Affine Hybrid Systems -- Reachability Problems on Extended O-Minimal Hybrid Automata -- Counterexamples for Timed Probabilistic Reachability -- Petri Nets -- Time Supervision of Concurrent Systems Using Symbolic Unfoldings of Time Petri Nets -- Comparison of the Expressiveness of Timed Automata and Time Petri Nets -- Semantics -- Quantifying Similarities Between Timed Systems -- Performance of Pipelined Asynchronous Systems -- Is Timed Branching Bisimilarity an Equivalence Indeed? -- Semantics and Modelling -- Implementation of Timed Automata: An Issue of Semantics or Modeling? -- Timed Abstract Non-interference. |
| Record Nr. | UNISA-996465550903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal Modeling and Analysis of Timed Systems : Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings / / edited by Paul Pettersson, Wang Yi
| Formal Modeling and Analysis of Timed Systems : Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings / / edited by Paul Pettersson, Wang Yi |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
| Descrizione fisica | 1 online resource (IX, 305 p.) |
| Disciplina | 005.1015113 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computer logic
Software engineering Programming languages (Electronic computers) Special purpose computers Logics and Meanings of Programs Software Engineering Programming Languages, Compilers, Interpreters Special Purpose and Application-Based Systems |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk -- Modular Performance Analysis of Distributed Embedded Systems -- Logic and Specification -- Real Time Temporal Logic: Past, Present, Future -- Translating Timed I/O Automata Specifications for Theorem Proving in PVS -- Specification and Refinement of Soft Real-Time Requirements Using Sequence Diagrams -- Times Games and Synthesis -- On Optimal Timed Strategies -- Average Reward Timed Games -- Beyond Liveness: Efficient Parameter Synthesis for Time Bounded Liveness -- Invited Talk -- Verification of Parameterized Timed Systems -- Model Checking -- Model Checking the Time to Reach Agreement -- Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems -- A New Verification Procedure for Partially Clairvoyant Scheduling -- Invited Talk -- Timing Analysis and Simulation Tools for Real-Time Control -- Hybrid Systems -- Automatic Rectangular Refinement of Affine Hybrid Systems -- Reachability Problems on Extended O-Minimal Hybrid Automata -- Counterexamples for Timed Probabilistic Reachability -- Petri Nets -- Time Supervision of Concurrent Systems Using Symbolic Unfoldings of Time Petri Nets -- Comparison of the Expressiveness of Timed Automata and Time Petri Nets -- Semantics -- Quantifying Similarities Between Timed Systems -- Performance of Pipelined Asynchronous Systems -- Is Timed Branching Bisimilarity an Equivalence Indeed? -- Semantics and Modelling -- Implementation of Timed Automata: An Issue of Semantics or Modeling? -- Timed Abstract Non-interference. |
| Record Nr. | UNINA-9910483853003321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
HSCC'10 : proceedings of the 13th ACM International Conference on hybrid systems : computation and control : April 12-15, 2010, Stockholm, Sweden
| HSCC'10 : proceedings of the 13th ACM International Conference on hybrid systems : computation and control : April 12-15, 2010, Stockholm, Sweden |
| Autore | Johansson Karl Henrik |
| Pubbl/distr/stampa | [Place of publication not identified] : , : Association for Computing Machinery, , 2010 |
| Descrizione fisica | 1 online resource (308 pages) |
| Disciplina | 629.8 |
| Collana | ACM Conferences. |
| Soggetto topico |
Hybrid systems
Hybrid computers Engineering & Applied Sciences Computer Science |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Altri titoli varianti | HSCC '10 |
| Record Nr. | UNINA-9910376070003321 |
Johansson Karl Henrik
|
||
| [Place of publication not identified] : , : Association for Computing Machinery, , 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Model Checking, Synthesis, and Learning [[electronic resource] ] : Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday / / edited by Ernst-Rüdiger Olderog, Bernhard Steffen, Wang Yi
| Model Checking, Synthesis, and Learning [[electronic resource] ] : Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday / / edited by Ernst-Rüdiger Olderog, Bernhard Steffen, Wang Yi |
| Edizione | [1st ed. 2021.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
| Descrizione fisica | 1 online resource (228 pages) |
| Disciplina | 004.0151 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Artificial intelligence Software engineering Microprogramming Computers, Special purpose Computer Science Logic and Foundations of Programming Artificial Intelligence Software Engineering Control Structures and Microprogramming Special Purpose and Application-Based Systems |
| ISBN | 3-030-91384-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Model Checking, Synthesis, and Learning -- From Linear Temporal Logics to Büchi Automata: The Early and Simple Principle -- Cause-Effect Reaction Latency In Real-Time Systems -- Quantitative Analysis of Interval Markov Chains -- Regular Model Checking: Evolution and Perspectives -- Regular Model Checking Revisited -- High-Level Representation of Benchmark Families for Petri Games -- Towards Engineering Digital Twinsby Active Behaviour Mining -- Never-Stop Context-Free Learning -- A Taxonomy and Reductions for Common Register Automata Formalisms. |
| Record Nr. | UNISA-996464431703316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Model Checking, Synthesis, and Learning : Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday / / edited by Ernst-Rüdiger Olderog, Bernhard Steffen, Wang Yi
| Model Checking, Synthesis, and Learning : Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday / / edited by Ernst-Rüdiger Olderog, Bernhard Steffen, Wang Yi |
| Edizione | [1st ed. 2021.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 |
| Descrizione fisica | 1 online resource (228 pages) |
| Disciplina | 004.0151 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Artificial intelligence Software engineering Microprogramming Computers, Special purpose Computer Science Logic and Foundations of Programming Artificial Intelligence Software Engineering Control Structures and Microprogramming Special Purpose and Application-Based Systems |
| ISBN | 3-030-91384-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Model Checking, Synthesis, and Learning -- From Linear Temporal Logics to Büchi Automata: The Early and Simple Principle -- Cause-Effect Reaction Latency In Real-Time Systems -- Quantitative Analysis of Interval Markov Chains -- Regular Model Checking: Evolution and Perspectives -- Regular Model Checking Revisited -- High-Level Representation of Benchmark Families for Petri Games -- Towards Engineering Digital Twinsby Active Behaviour Mining -- Never-Stop Context-Free Learning -- A Taxonomy and Reductions for Common Register Automata Formalisms. |
| Record Nr. | UNINA-9910512155003321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2021 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001 Proceedings / / edited by Tiziana Margaria, Wang Yi
| Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001 Proceedings / / edited by Tiziana Margaria, Wang Yi |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XIV, 594 p.) |
| Disciplina | 004.2/11 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer logic Computer communication systems Algorithms Software Engineering/Programming and Operating Systems Logics and Meanings of Programs Software Engineering Computer Communication Networks Algorithm Analysis and Problem Complexity |
| ISBN | 3-540-45319-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- Branching vs. Linear Time: Final Showdown -- Propositional Reasoning -- Symbolic Verification -- Language Containment Checking with Nondeterministic BDDs -- Satisfiability Checking Using Boolean Expression Diagrams -- A Library for Composite Symbolic Representations -- Infinite State Systems: Deduction and Abstraction -- Synthesis of Linear Ranking Functions -- Automatic Deductive Verification with Invisible Invariants -- Incremental Verification by Abstraction -- A Technique for Invariant Generation -- Application of Model Checking Techniques -- Model Checking Syllabi and Student Careers -- Verification of Vortex Workflows -- Parameterized Verification of Multithreaded Software Libraries -- Timed and Probabilistic Systems -- Efficient Guiding Towards Cost-Optimality in UPPAAL -- Linear Parametric Model Checking of Timed Automata -- Abstraction in Probabilistic Process Algebra -- First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders -- Hardware: Design and Verification -- Hardware/Software Co-design Using Functional Languages -- Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors -- Software Verification -- Boolean and Cartesian Abstraction for Model Checking C Programs -- Finding Feasible Counter-examples when Model Checking Abstracted Java Programs -- The loop Compiler for Java and JML -- Symbolic Verification -- Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking -- Saturation: An Efficient Iteration Strategy for Symbolic State—Space Generation -- Testing: Techniques and Tools -- Automated Test Generation from Timed Automata -- Testing an Intentional Naming Scheme Using Genetic Algorithms -- Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions -- TATOO: Testing and Analysis Tool for Object-Oriented Software -- Implementation Techniques -- Implementing a Multi-valued Symbolic Model Checker -- Is There a Best Symbolic Cycle-Detection Algorithm? -- Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets -- A Sweep-Line Method for State Space Exploration -- Semantics and Compositional Verification -- Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams -- Simulation Revisited -- Compositional Message Sequence Charts -- An Automata Based Interpretation of Live Sequence Charts -- Logics and Model-Checking -- Coverage Metrics for Temporal Logic Model Checking -- Parallel Model Checking for the Alternation Free ?-Calculus -- Model Checking CTL*[DC] -- ETAPS Tool Demonstration -- CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS -- The ASM Workbench: A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models -- The Erlang Verification Tool. |
| Record Nr. | UNISA-996465708203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Tools and Algorithms for the Construction and Analysis of Systems : 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001 Proceedings / / edited by Tiziana Margaria, Wang Yi
| Tools and Algorithms for the Construction and Analysis of Systems : 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001 Proceedings / / edited by Tiziana Margaria, Wang Yi |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XIV, 594 p.) |
| Disciplina | 004.2/11 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer logic Computer communication systems Algorithms Software Engineering/Programming and Operating Systems Logics and Meanings of Programs Software Engineering Computer Communication Networks Algorithm Analysis and Problem Complexity |
| ISBN | 3-540-45319-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- Branching vs. Linear Time: Final Showdown -- Propositional Reasoning -- Symbolic Verification -- Language Containment Checking with Nondeterministic BDDs -- Satisfiability Checking Using Boolean Expression Diagrams -- A Library for Composite Symbolic Representations -- Infinite State Systems: Deduction and Abstraction -- Synthesis of Linear Ranking Functions -- Automatic Deductive Verification with Invisible Invariants -- Incremental Verification by Abstraction -- A Technique for Invariant Generation -- Application of Model Checking Techniques -- Model Checking Syllabi and Student Careers -- Verification of Vortex Workflows -- Parameterized Verification of Multithreaded Software Libraries -- Timed and Probabilistic Systems -- Efficient Guiding Towards Cost-Optimality in UPPAAL -- Linear Parametric Model Checking of Timed Automata -- Abstraction in Probabilistic Process Algebra -- First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders -- Hardware: Design and Verification -- Hardware/Software Co-design Using Functional Languages -- Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors -- Software Verification -- Boolean and Cartesian Abstraction for Model Checking C Programs -- Finding Feasible Counter-examples when Model Checking Abstracted Java Programs -- The loop Compiler for Java and JML -- Symbolic Verification -- Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking -- Saturation: An Efficient Iteration Strategy for Symbolic State—Space Generation -- Testing: Techniques and Tools -- Automated Test Generation from Timed Automata -- Testing an Intentional Naming Scheme Using Genetic Algorithms -- Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions -- TATOO: Testing and Analysis Tool for Object-Oriented Software -- Implementation Techniques -- Implementing a Multi-valued Symbolic Model Checker -- Is There a Best Symbolic Cycle-Detection Algorithm? -- Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets -- A Sweep-Line Method for State Space Exploration -- Semantics and Compositional Verification -- Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams -- Simulation Revisited -- Compositional Message Sequence Charts -- An Automata Based Interpretation of Live Sequence Charts -- Logics and Model-Checking -- Coverage Metrics for Temporal Logic Model Checking -- Parallel Model Checking for the Alternation Free ?-Calculus -- Model Checking CTL*[DC] -- ETAPS Tool Demonstration -- CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS -- The ASM Workbench: A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models -- The Erlang Verification Tool. |
| Record Nr. | UNINA-9910768474203321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||