Safe and Secure Systems - Tools
VSE - Verification Support Environment
VSE supports formal development in a comprehensive way by closely integrating specification, deduction, and management of developments. It was developed in two phases for the German Information Security Agency (Bundesamt für Sicherheit in der Informationstechnik, BSI) by a consortium from industry and academia. The main motivation was to make available an industrial strength tool for developments satisfying the highest assurance levels (of ITSEC and CC). In fact, the system has been applied and used in large commercial projects in that area. However, the VSE is not restricted to security issues: it provides a general methodology for a modular formal development that starts with abstract specifications and proceeds by stepwise refinement to the formal description of more concrete layers even down to the code level.
VSE offers implemented development methods for sequential algorithms and distributed concurrent systems using first-order abstract data types, Dynamic Logic, and Temporal Logic as basic building blocks. Structured developments are represented as so called development graphs that serve as an interface to the deduction component. Current work on VSE is concerned with the integration of specialized modelling techniques, as, for example, real-time and security models, and deductive techniques, like Automated Theorem Proving and Model Checking.
MAYA - Management of Change based on Development Graphs
The MAYA-system supports an evolutionary formal development since it allows users to specify and verify developments in a structured manner, incorporates a uniform mechanism for verification in-the-large to exploit the structure of the specification, and maintains the verification work already done when changing the specification. MAYA relies on development graphs as a uniform representation of structured specifications, which enables the use of various (structured) specification languages like CASL and VSE-SL to formalise the software development. To this end MAYA provides a generic interface to plug in additional parsers for the support of other specification languages. Moreover, MAYA allows the integration of different theorem provers to deal with the actual proof obligations arising from the specification, i.e. to perform verification in-the-small.
Textual specifications are translated into a structured logical representation called a development graph, which is based on the notions of consequence relations and morphisms and makes arising proof obligations explicit. The user can tackle these proof obligations with the help of theorem provers connected to MAYA like Isabelle or Inka.