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.
Automated Technology for Verification and Analysis [[electronic resource] ] : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009, Proceedings / / edited by Zhiming Liu, Anders P. Ravn
| Automated Technology for Verification and Analysis [[electronic resource] ] : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009, Proceedings / / edited by Zhiming Liu, Anders P. Ravn |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (XI, 414 p.) |
| Disciplina | 004n/a |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Computers
Computer programming Programming languages (Electronic computers) Computer logic Mathematical logic Algorithms Theory of Computation Programming Techniques Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Algorithm Analysis and Problem Complexity |
| Soggetto genere / forma |
Kongress.
Macao (2009) |
| ISBN | 3-642-04761-0 |
| Classificazione |
DAT 286f
DAT 325f DAT 704f SS 4800 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Verifying VLSI Circuits -- 3-Valued Abstraction for (Bounded) Model Checking -- Local Search in Model Checking -- State Space Reduction -- Exploring the Scope for Partial Order Reduction -- State Space Reduction of Linear Processes Using Control Flow Reconstruction -- A Data Symmetry Reduction Technique for Temporal-epistemic Logic -- Tools -- TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets -- CLAN: A Tool for Contract Analysis and Conflict Discovery -- UnitCheck: Unit Testing and Model Checking Combined -- Probabilistic Systems -- LTL Model Checking of Time-Inhomogeneous Markov Chains -- Statistical Model Checking Using Perfect Simulation -- Quantitative Analysis under Fairness Constraints -- A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems -- Medley -- Memory Usage Verification Using Hip/Sleek -- Solving Parity Games in Practice -- Automated Analysis of Data-Dependent Programs with Dynamic Memory -- Temporal Logic I -- On-the-fly Emptiness Check of Transition-Based Streett Automata -- On Minimal Odd Rankings for Büchi Complementation -- Specification Languages for Stutter-Invariant Regular Properties -- Abstraction and Refinement -- Incremental False Path Elimination for Static Software Analysis -- A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement -- Don’t Know for Multi-valued Systems -- Logahedra: A New Weakly Relational Domain -- Fault Tolerant Systems -- Synthesis of Fault-Tolerant Distributed Systems -- Formal Verification for High-Assurance Behavioral Synthesis -- Dynamic Observers for the Synthesis of Opaque Systems -- Temporal Logic II -- Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation -- LTL Model Checking for Recursive Programs -- On Detecting Regular Predicates in Distributed Systems. |
| Record Nr. | UNISA-996465383803316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
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 | ||
| ||
Domain Modeling and the Duration Calculus : International Training School, Shanghai, China, September 17-21, 2007, Advanced Lectures / / edited by Chris George, Zhiming Liu, Jim Woodcock
| Domain Modeling and the Duration Calculus : International Training School, Shanghai, China, September 17-21, 2007, Advanced Lectures / / edited by Chris George, Zhiming Liu, Jim Woodcock |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XI, 240 p.) |
| Disciplina | 004.33 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computer systems Computer science Computer networks Algorithms Software Engineering Computer System Implementation Computer Science Logic and Foundations of Programming Computer Communication Networks |
| ISBN | 3-540-74964-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Delivering Real-Time Behaviour -- Applicative Modelling with RAISE -- A Theory of Duration Calculus with Application -- Understanding Programming Language Concepts Via Operational Semantics. |
| Record Nr. | UNINA-9910485022703321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Domain Modeling and the Duration Calculus : International Training School, Shanghai, China, September 17-21, 2007, Advanced Lectures / / edited by Chris George, Zhiming Liu, Jim Woodcock
| Domain Modeling and the Duration Calculus : International Training School, Shanghai, China, September 17-21, 2007, Advanced Lectures / / edited by Chris George, Zhiming Liu, Jim Woodcock |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XI, 240 p.) |
| Disciplina | 004.33 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Computer systems Computer science Computer networks Algorithms Software Engineering Computer System Implementation Computer Science Logic and Foundations of Programming Computer Communication Networks |
| ISBN | 3-540-74964-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Delivering Real-Time Behaviour -- Applicative Modelling with RAISE -- A Theory of Duration Calculus with Application -- Understanding Programming Language Concepts Via Operational Semantics. |
| Record Nr. | UNISA-996466093703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Engineering Trustworthy Software Systems [[electronic resource] ] : 5th International School, SETSS 2019, Chongqing, China, April 21–27, 2019, Tutorial Lectures / / edited by Jonathan P. Bowen, Zhiming Liu, Zili Zhang
| Engineering Trustworthy Software Systems [[electronic resource] ] : 5th International School, SETSS 2019, Chongqing, China, April 21–27, 2019, Tutorial Lectures / / edited by Jonathan P. Bowen, Zhiming Liu, Zili Zhang |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
| Descrizione fisica | 1 online resource (XVII, 221 p. 32 illus.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer communication systems Artificial intelligence Computer programming Architecture, Computer Natural language processing (Computer science) Software Engineering/Programming and Operating Systems Computer Communication Networks Artificial Intelligence Programming Techniques Computer System Implementation Natural Language Processing (NLP) |
| ISBN | 3-030-55089-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Seamless Model-based System Development: Foundations -- From Bounded Reachability Analysis of Linear Hybrid Automata to Verification of Industrial CPS and IoT -- Weakest Preexpectation Semantics for Bayesian Inference: Conditioning, Continuous Distributions and Divergence -- K - A Semantic Framework for Programming Languages and Formal Analysis Tools -- Software Abstractions and Human-Cyber-Physical Systems Architecture Modelling. |
| Record Nr. | UNISA-996418305803316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Engineering Trustworthy Software Systems : 5th International School, SETSS 2019, Chongqing, China, April 21–27, 2019, Tutorial Lectures / / edited by Jonathan P. Bowen, Zhiming Liu, Zili Zhang
| Engineering Trustworthy Software Systems : 5th International School, SETSS 2019, Chongqing, China, April 21–27, 2019, Tutorial Lectures / / edited by Jonathan P. Bowen, Zhiming Liu, Zili Zhang |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
| Descrizione fisica | 1 online resource (XVII, 221 p. 32 illus.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer communication systems Artificial intelligence Computer programming Architecture, Computer Natural language processing (Computer science) Software Engineering/Programming and Operating Systems Computer Communication Networks Artificial Intelligence Programming Techniques Computer System Implementation Natural Language Processing (NLP) |
| ISBN | 3-030-55089-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Seamless Model-based System Development: Foundations -- From Bounded Reachability Analysis of Linear Hybrid Automata to Verification of Industrial CPS and IoT -- Weakest Preexpectation Semantics for Bayesian Inference: Conditioning, Continuous Distributions and Divergence -- K - A Semantic Framework for Programming Languages and Formal Analysis Tools -- Software Abstractions and Human-Cyber-Physical Systems Architecture Modelling. |
| Record Nr. | UNINA-9910413437403321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Engineering Trustworthy Software Systems : 4th International School, SETSS 2018, Chongqing, China, April 7–12, 2018, Tutorial Lectures / / edited by Jonathan P. Bowen, Zhiming Liu, Zili Zhang
| Engineering Trustworthy Software Systems : 4th International School, SETSS 2018, Chongqing, China, April 7–12, 2018, Tutorial Lectures / / edited by Jonathan P. Bowen, Zhiming Liu, Zili Zhang |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XVII, 237 p. 556 illus., 84 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer communication systems Algorithms Computer logic Mathematical logic Artificial intelligence Software Engineering Computer Communication Networks Algorithm Analysis and Problem Complexity Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
| ISBN | 3-030-17601-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An Introduction to Software Verification with Whiley -- Learning Büchi Automata and Its Applications -- Securing Emergent IoT Applications -- Programming Z3 -- The Impact of Alan Turing: Formal Methods and Beyond. . |
| Record Nr. | UNISA-996466303703316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Engineering Trustworthy Software Systems : 4th International School, SETSS 2018, Chongqing, China, April 7–12, 2018, Tutorial Lectures / / edited by Jonathan P. Bowen, Zhiming Liu, Zili Zhang
| Engineering Trustworthy Software Systems : 4th International School, SETSS 2018, Chongqing, China, April 7–12, 2018, Tutorial Lectures / / edited by Jonathan P. Bowen, Zhiming Liu, Zili Zhang |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XVII, 237 p. 556 illus., 84 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer communication systems Algorithms Computer logic Mathematical logic Artificial intelligence Software Engineering Computer Communication Networks Algorithm Analysis and Problem Complexity Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
| ISBN | 3-030-17601-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An Introduction to Software Verification with Whiley -- Learning Büchi Automata and Its Applications -- Securing Emergent IoT Applications -- Programming Z3 -- The Impact of Alan Turing: Formal Methods and Beyond. . |
| Record Nr. | UNINA-9910337563003321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Engineering Trustworthy Software Systems [[electronic resource] ] : Third International School, SETSS 2017, Chongqing, China, April 17–22, 2017, Tutorial Lectures / / edited by Jonathan P. Bowen, Zhiming Liu, Zili Zhang
| Engineering Trustworthy Software Systems [[electronic resource] ] : Third International School, SETSS 2017, Chongqing, China, April 17–22, 2017, Tutorial Lectures / / edited by Jonathan P. Bowen, Zhiming Liu, Zili Zhang |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XVII, 219 p. 127 illus., 31 illus. in color.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer programming Computer logic Computers Computer system failures Software Engineering Programming Languages, Compilers, Interpreters Programming Techniques Logics and Meanings of Programs The Computing Profession System Performance and Evaluation |
| ISBN | 3-030-02928-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | A Guide to Rely/Guarantee Thinking -- An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping -- Formalizing Hoare Logic in PVS -- Modeling Concurrency in Dafny -- Software Is Not Soft: Challenges and Approaches to Dynamic Software Update -- Challenges for Formal Semantic Description: Responses from the Main Approaches. . |
| Record Nr. | UNISA-996466277303316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
