FORMAL VERIFICATION OF RECONFIGURABLE SYTEMS

project  PN-III-P2-2.1-PED-2016-0494, funded by UEFISCDI under contract


Domain 2. Information and communication technologies, space and security
Subdomain 2.1 Information and Communication Technologies

Project scope

The field of formal specification and verification of software and hardware systems is without alternative in safety-critical or security areas where one cannot take the risk of failure. This includes several success stories such as the verification of the Pentium IV arithmetic, the verification of the Traffic Collision Avoidance System TCAS, various security protocols, etc. In many cases, only the use of logic-based techniques has been able to reveal serious bugs in software and hardware systems; in other cases, spectacular and costly failures such as the loss of the Mars Climate Orbiter could have been avoided by formal techniques. Moreover it is well established that formal support greatly enhances the efficiency of software development and maintenance.
An important class of software systems are the reconfigurable ones; these are software systems that behave differently in different modes of operation (often called configurations) and commute between them along their lifetime. Such systems, which evolve in response to external or internal stimulus, are everywhere: from e-Health or e-Government integrated services to sensor networks, from domestic appliances to complex systems distributed and collaborating over the web, from safety or mission-critical applications to massive parallel software.
The goal of this project is to develop an integrated formal specification and verification environment for reconfigurable systems that include a (1) dedicated generic logic-based specification language, (2) a formal verification tool, (3) a set of methodologies for using the specification and the verification tools and (4) a library of examples and case studies. The environment is meant to be used both as a working tool in industry and as educational tool in universities and research centers.

▲

Members

Răzvan Diaconescu
CS1, project director (Simion Stoilow Institute of Mathematics of the Romanian Academy – IMAR)
Mihai Codescu
Postodoctoral Researcher (Simion Stoilow Institute of Mathematics of the Romanian Academy – IMAR)
▲

References

The technology of the project is based on joining two base sub-technologies, namely the mathematical model of hybridized institutions and the Hets system of tools. The base references for these are:
  1. R. Diaconescu, P. Stefaneas: Ultraproducts and possible worlds semantics in institutions, Theoretical Computer Science 379:210-230, Elsevier (2007)
  2. R. Diaconescu, A. Madeira: Encoding hybridized institutions into first order logic, Mathematical Structures in Computer Science 26:745-788, Cambridge University Press (2016)
  3. T. Mossakowski, C. Maeder, K. Luttich: The Heterogeneous Tool Set, in O. Grumberg and M. Huth (Eds.): TACAS 2007, Lecture Notes in Computer Science 4424:519-522, Springer (2007).
▲
▲

Scientific Reports

  1. Scientific Report of the project for the period Aug. 2017 - Dec. 2017
  2. Scientific Report of the project for 2018
  3. Scientific Report of the project for the whole duration of the project
▲

Events

  1. visit of M. Codescu at the Hets group in Magdeburg, 30.10.2017 - 19.11.2017
  2. visit of R. Diaconescu at the Hets group in Magdeburg, 26.11.2017 - 9.12.2017
▲
  1. The H system (including documentation, executables, libraries of examples and case study)
▲