Hybrid systems with both discrete and continuous dynamics are an important model for real-world cyber-physical systems. The key challenge is to ensure their correct functioning w.r.t. safety requirements. Promising techniques to ensure safety seem to be model-driven engineering to develop hybrid systems in a well-defined and traceable manner, and formal verification to prove their correctness. Their combination forms the vision of verification-driven engineering. Often, hybrid systems are rather complex in that they require expertise from many domains (e. g., robotics, control systems, computer science, software engineering, and mechanical engineering). Moreover, despite the remarkable progress in automating formal verification of hybrid systems, the construction of proofs of complex systems often requires nontrivial human guidance, since hybrid systems verification tools solve undecidable problems. It is, thus, not uncommon for development and verification teams to consist of many players with diverse expertise. This paper introduces a verification-driven engineering toolset that extends our previous work on hybrid and arithmetic verification with tools for (1) graphical (UML) and textual modeling of hybrid systems, (2) exchanging and comparing models and proofs, and (3) managing verification tasks. This toolset makes it easier to tackle large-scale verification tasks.
@cite_18: In modular verification the specification of a module consists of two parts. One hart describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system iii which the module is interacting. This is called the assume-guarantee paradigm. In this paper we consider assume-guarantee specifications in which the guarantee is specified by branching temporal formulas. We distinguish between two approaches. In the first approach, the assumption is specified by branching temporal formulas. In the second approach, the assumption is specified by linear temporal logic. We consider guarantees in ∀CTL and ∀CTL * , the universal fragments of CTL and CTL * , and assumptions in LTL. ∀CTL, and ∀CTL * . We describe a reduction of modular model checking to standard model checking. Using the reduction, we show that modular model checking is PSPACE-complete for ∀CTL and is EXPSPACE-complete for ∀CTL * . We then show that the case of LTL assumption is a special case of the case of ∀CTL * assumption, but that the EXPSPACE-hardness result apply already to assumptions in LTL.
@cite_4: We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute an over-approximation of the reachable states. The algorithm improves over previous work by using variable time steps to guarantee a given local error bound. In addition, we propose an improved approximation model, which drastically improves the accuracy of the algorithm. The algorithm is implemented as part of SpaceEx, a new verification platform for hybrid systems, available at spaceex.imag.fr. Experimental results of full fixed-point computations with hybrid systems with more than 100 variables illustrate the scalability of the approach.
@cite_41: Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.
@cite_29: An overview of various modeling frameworks for hybrid systems is given followed by a comparison of the modeling power and the model complexity, which can serve as a guideline for choosing the right model for a given analysis or control problem with hybrid dynamics. Then, the main analydsis and design tasks for hybrid system.s are surveyed together with the methods for their solution, which will be discussed in more detail in subsequent chapters.
@cite_53: The 'Polymath Project' proved that many minds can work together to solve difficult mathematical problems. Timothy Gowers and Michael Nielsen reflect on the lessons learned for open-source science.
@cite_1: Many mainstream static code checkers make a number of compromises to improve automation, performance, and accuracy. These compromises include not checking certain program properties as well as making implicit, unsound assumptions. Consequently, the results of such static checkers do not provide definite guarantees about program correctness, which makes it unclear which properties remain to be tested. We propose a technique for collaborative verification and testing that makes compromises of static checkers explicit such that they can be compensated for by complementary checkers or testing. Our experiments suggest that our technique finds more errors and proves more properties than static checking alone, testing alone, and combinations that do not explicitly document the compromises made by static checkers. Our technique is also useful to obtain small test suites for partially-verified programs.
@cite_39: In formal verification, a designer first constructs a model, with mathematically precise semantics, of the system under design, and performs extensive analysis with respect to correctness requirements. The appropriate mathematical model for embedded control systems is hybrid systems that combines the traditional state-machine based models for discrete control with classical differential-equations based models for continuously evolving physical activities. In this article, we briefly review selected existing approaches to formal verification of hybrid systems, along with directions for future research.
@cite_0: One of the central axioms of extreme programming is the disciplined use of regression testing during stepwise software development. Due to recent progress in software model checking, it has become possible to supplement this process with automatic checks for behavioral safety properties of programs, such as conformance with locking idioms and other programming protocols and patterns. For efficiency reasons, all checks must be incremental, i. e., they must reuse partial results from previous checks in order to avoid all unnecessary repetition of expensive verification tasks. We show that the lazy-abstraction algorithm, and its implementation in Blast, can be extended to support the fully automatic and incremental checking of temporal safety properties during software development.
@cite_59: This paper focuses on the challenges of modeling cyber-physical systems (CPSs) that arise from the intrinsic heterogeneity, concurrency, and sensitivity to timing of such systems. It uses a portion of an aircraft vehicle management system (VMS), specifically the fuel management subsystem, to illustrate the challenges, and then discusses technologies that at least partially address the challenges. Specific technologies described include hybrid system modeling and simulation, concurrent and heterogeneous models of computation, the use of domain-specific ontologies to enhance modularity, and the joint modeling of functionality and implementation architectures.
@cite_12: In 1995, HyTech broke new ground as a potentially powerful tool for verifying hybrid systems – yet it has remained severely limited in its applicability to more complex systems. We address the main problems of HyTech with PHAVer, a new tool for the exact verification of safety properties of hybrid systems with piecewise constant bounds on the derivatives. Affine dynamics are handled by on-the-fly overapproximation and by partitioning the state space based on user-definable constraints and the dynamics of the system. PHAVer's exact arithmetic is robust due to the use of the Parma Polyhedra Library, which supports arbitrarily large numbers. To manage the complexity of the polyhedral computations, we propose methods to conservatively limit the number of bits and constraints of polyhedra. Experimental results for a navigation benchmark and a tunnel diode circuit show the effectiveness of the approach.
Recent surveys on verification methods for hybrid systems @cite_39 , modeling and analysis of hybrid systems @cite_29 , and modeling of cyber-physical systems @cite_59 , reveal that indeed many tools are available for modeling and analyzing hybrid systems, but in a rather isolated manner. Supporting collaboration on formal verification by distributing tasks among members of a verification team in a model-driven engineering approach has not yet been the focus. Although current verification tools for hybrid systems ( , PHAVer @cite_12 , SpaceEx @cite_4 ), as well as those for arithmetic ( , Z3 @cite_41 ) are accompanied by modeling editors of varying sophistication, they are not yet particularly well prepared for collaboration either. Developments in collaborative verification of source code by multiple complementary static code checkers @cite_1 , modular model-checking ( , @cite_18 ), and extreme verification @cite_0 , however, indicate that this is indeed an interesting field. Most notably, usage of online collaboration tools in the Polymath project has led to an elementary proof of a special case of the density Hales-Jewett theorem @cite_53 .