Description
The InvariantChecker can be used to statically verify safety properties for system specifications. The properties that could be verified have to be state properties - i.e. they are only evaluated for a single state. For such properties the InvariantChecker checks, whether or not they are an inductive invariant of the system specification. An important fact is that an inducitve invariant is, in contrast to an operative invariant, independent of the system's reachable states. Thus, the InvariantChecker over approximates the system's state space what might yield so called false-negatives. The basic idea behind the InvariantChecking approach is to reverse apply graph transformation rules to minimal unsafe situations. If the resulting situation is a safe situation, the system specification to verify is unsafe, as it potentially contains transitions from safe to unsate situations.
InvariantChecker package structure and dependencies
The InvariantChecker has been extended to be also able to verify hybrid systems. The class of hybrid systems that can be verified using the InvariantChecker depends on the solver that is used. In a first version we used constraint logic programming and thus we were restricted to linear hybrid systems, whereas linear means variables have to be multiplied with scalars only. An extension to also use PHaver as a solver for the differential equations allows us to increase the expressiveness, concerning the continuous behavior. PHaver supports the analysis of linear differential equations, wich allow mutliplications between two variables.
Further, the InvariantChecker has been extended to support the verification of preserved properties. Using this extension we can show that all states of system specification contain at least one occurrence of a preserved properties.
The InvariantChecker software is subject to constant improvement and ongoing development and available upon request. Due to license issues we can not distribute the extension for hybrid systems.
Project Team
- Leen Lambers
- Sven Schneider (contact person)
Former Team Members:
Software
- InvariantChecker
Supported Languages
- SamiGra