FormalSafe: Formal Development for Safe Robotics
FormalSafe aims at computer-aided management of the many types of documents involved in the development of highly dependable systems, applied to the area of safe robotics. The Document Management and Tool Integration Platform (DocTIP) will keep track of the various dependencies in and between such documents to provide efficient change management.
Specialised tools can be plugged in to explore the semantics of particular documents, and to reason about relations between document parts. Research topics are the development of a generic framework to maintain structured informal, semi-formal and formal documents, the transfer and integration of existing reasoning approaches, and abstraction for reuse of developments. The general approach will be instantiated with two application scenarios in the area of robotics.
FormalSafe's agile formal development model will enable shorter development cycles without compromising safety, leading to shorter time-to-market and increased competitivity.
Work Area: Formal Methods: To support the envisaged formal parts of the safe technical development process, we aim at the integration of formal languages and tools in a ﬂexible framework with a clear semantical basis. This tool framework, DocTIP, will be an extension of the HeTS system, developed over the last years in the Safe and Secure Cognitive Systems (SKS) group now based in Bremen. Its semantic basis is abstract model theory, where different formalisms (logics) are modelled as so-called institutions, and the translations between them as institution co-morphisms. HeTS manages proof obligations and proofs across the different formalisms, and allows the recognition of sub-languages and the selection of available tools for efficient tool support, accordingly.
DocTIP will offer a well-developed and stable core of industrial-strength logics and tools, centred around the wide-spectrum language HO-Casl (aka HasCASL developed at SKS as well), the interactive theorem provers Isabelle, HOL Light, and VSE, as well as various fully automated theorem provers. We will adapt this framework to deal with problems speciﬁc to the engineering and robotics domain, in particular integrate support for geometric problems, calculus, and numerics, as well as for C as a domain-typical programming language.
The DocTIP framework will moreover provide interfaces to the change management layer of FormalSafe, including in particular an extended proof management. Thus, a comprehensive and user-friendly environment for formal software development is created.
Work Area: Semantic Document Management: This work area is concerned with the development of methodologies, techniques and tools for a semantic document management. From a document-centered point of view, a software development process can be considered as the evolution of a family of documents that are semantically intertwined by various formal and informal dependencies but also written in different languages with different degrees of formalization. While the semantics of program code or formal specifications is formally given by the corresponding operational semantics of the programming language or the underlying logic used for the specification, the semantics of e.g. documentations or requirements, written in natural language, defy a thorough formal semantic interpretation. However, although such documents are written in a non-formal language, they typically expose an internal (syntactical) structure which conforms to the structure of its informal semantics. In this spirit documents written in non-formal languages can provide a formal structuring allowing the formulation of ﬁne-grained dependencies between documents with different degrees of formalization.
FormalSafe aims to utilise such properties for a semantic document management that allows the user to specify or postulate dependencies or the non-interference of document parts, to maintain these properties for a consistent evolution of the documents, and to automate development steps, the tasks of which are sufficiently formally specified.
Work Area: Abstraction for Reuse: Our tool suite will cover all aspects of reuse, from the reuse of single modules over comprehensive change management up to abstraction for reuse. Whereas the reuse of modules, programs and components is well-known and widely used, abstraction for reuse, the focus of this work area, is a novel concept. Its foundations have been investigated in the AWE project at the Universität Bremen. Abstraction for reuse describes the process of systematically making a given development more general, in order to be able to reuse it in a different, yet similar setting.
The AWE project has investigated this process in the context of formal methods, and more particular in the context of proofs. We have identified several operations to make a formal development or proof more general, such as making a theorem used in the proof an explicit assumption, replacing a constant by a variable, or replacing a type by a free type variable. A prototypical implementation of the concept based on the Isabelle theorem prover is available, which allows manipulation of Isabelle theorems based on proof term transformations. The work in this area will build on this foundational work. We want to extend our tool suite with abstraction capabilities for formal and even semi-formal methods, and explore the applicability of this approach to areas such as technical documents (CAD documents).
Work Area: Basic Infrastructure: This work area is concerned with providing basic infrastructure that is needed in the FormalSafe project. The focus is not on original research, but on selecting existing best practices and adpating them to the needs of DocTIP. A crucial goal is to realise a set of loosely coupled tools that all use the same data interchanged formats and protocols, that refer to a common versioned database, and that provide uniform user interfaces. We also develop Eclipse support for the different document types supported by DocTIP: the webpage of these plugins is here.
Work Area: Application Scenarios Rolland and VI-Bot
List of Upcoming Internal Talks
This is the schedule of upcoming short informal talks about completed work to be held as part of the weekly FormalSafe? meeting:
- 12.5 Serge, Normen: Change Management
- 19.5 Lutz, Ewaryst und Dominik: CAS-Einbindung und CAD-Verifikation für den WADT.
- 26.5 Andrea, Michael: Multidimensionalität von Formalität - Erfahrungen mit der Formalisierung der SAMS Dokumente
- 2.6 Till, Michael: Latin
- 16.6 Dominik, Christian und *Lutz*: partielle Funktionen und Isabelle.
- 23.6 Serge, Dodi: Dekl. Taktikskripte , evtl. dekl. Spec. Skripte
- 25.8 Lutz, Michael, Ewaryst: Formale Methoden für CAD
- 1.9 Till: Common Logic
- 8.9 Michael, Till, Florian: Latin reloaded
- 9.11 Serge, Dominik: DocTIP Demo
- 23.11 Ewaryst: Parameter Eliminationsverfahren Demo
- Serge, Till, Dieter: Construction-aware Development Graphs as a basis for change management
- Lutz: koalgebraische Logik