COMPONENT-BASED FORMAL VERIFICATION

project PN-III-P2-2.1-PED-2019-0955, funded by UEFISCDI under contract 404PED/2020


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

Project summary

The field of formal specification and verification of software and hardware systems is without alternative in safety-critical or security areas of system development where one cannot take the risk of failure. This applies to medical areas, aviation, military, etc., and in general to any area where human life cannot be compromised. One of the system-development techniques that may benefit naturally from using formal methods is component-based software engineering. This represents one of the modern realizations of the very important and all-pervading engineering principle of modularization. The goal of this project is to develop an integrated formal-specification-and-verification environment for component-based system development that includes:

This project's commitment to accommodate component-based systems makes the proposed toolset specifically well suited for dealing with object-oriented technologies, which have already become so prevalent across the industry. From the perspective of formal verification, the methodological highlight of the project is that all verifications will be performed in a fully automatic manner – that is, it will offer a kind of push-button technology, with a smooth learning curve, and a minimal to no need for the user to intervene during the verification. Therefore, the tool we set out to deliver will provide an integrated system-development environment with a solid mathematical foundation and, through automation, with no compromise of its ease of use; this will enable us to promote the toolset as a basis for further developing a working tool in the industry and/or an educational tool for universities and research centres alike.

▲

Members

Răzvan Diaconescu
CS1, project director (Simion Stoilow Institute of Mathematics of the Romanian Academy – IMAR)
Ionuț Țuțu
CS3, member (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 behavioural specification of hierarchical object composition and the Maude programming environment. The base references for these are:

  1. R. Diaconescu: Behavioural specification for hierarchical object composition, Theoretical Computer Science 343(3):305-331, Elsevier (2005)
  2. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework, Springer (2007)
▲
▲

Scientific Reports

  1. Scientific Report of the project for the period Oct. 2020 – Dec. 2021
  2. Scientific Report of the project for the period Jan. 2022 – Oct. 2022
  3. Final Project Report
▲

Events

▲

Project implementation and deliverables

Stage 1: COMP language definition (2020)

This includes the following planned deliverables, which have all been fully realized:

Stage 2: Methodologies and code generation (2021)

This includes the following planned deliverables, which have all been fully realized:

  • Specification and verification methodologies for using the COMP system
  • The COMP toolset, including a parser, static analyser, and code generator
  • The COMP reference manual, which covers all technical aspects of the language
Stage 3: Formal verification (2022)

This includes the following planned deliverables, which have all been fully realized:

▲
▲