A verification-driven framework for iterative design of controllers

DOI10.1007/s00165-019-00484-1zbMath1425.68262OpenAlexW2948911651WikidataQ127749078 ScholiaQ127749078MaRDI QIDQ2335947

Claudio Menghi, Marsha Chechik, Paola Spoletini, Carlo Ghezzi

Publication date: 18 November 2019

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-019-00484-1

zbMATH Keywords

controller designdistributed developmentverification-driven development

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Theory of software (68N99)

Related Items (2)

Integrating Topological Proofs with Model Checking to Instrument Iterative Design ⋮ TOrPEDO : witnessing model correctness with topological proofs

Uses Software

• Dafny
• NuSMV
• Why3
• VCC
• VeriFast
• WhyML
• KeY
• Viper
• Supremica
• OpenJML
• Antichains
• AutoProof

Cites Work

• Compatibility in a multi-component environment
• Weak, strong, and strong cyclic planning via symbolic model checking
• Data structures for symbolic multi-valued model-checking
• Verification of evolving software via component substitutability analysis
• Statecharts: a visual formalism for complex systems
• Reasoning about infinite computations
• Multi-robot LTL planning under uncertainty
• Dealing with incompleteness in automata-based model checking
• Supporting verification-driven incremental distributed design of components
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Automata for Specifying and Orchestrating Service Contracts
• Dafny: An Automatic Program Verifier for Functional Correctness
• Tentative steps toward a development method for interfering programs
• Formal verification of parallel programs
• Compositional Synthesis of Reactive Controllers for Multi-agent Systems
• Distribution of Modal Transition Systems
• From Model Checking to a Temporal Proof for Partial Models
• Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis
• Constraint-Based Verification
• Why3 — Where Programs Meet Provers
• Experimental Evaluation of Classical Automata Constructions
• Software Product Line Engineering
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A verification-driven framework for iterative design of controllers