VeriSpec - Structured Specification and Automated Verification for Automotive Functional Safety

The need for more advanced formal methodologies for design, development and verification of embedded systems has been identified by both industry and academia. VeriSpec will develop new, as well as adapt existing, modelling and verification techniques and relevant tool support for the analysis of requirements and architectural models of automotive systems, which could be seamlessly integrated within the industrial methodology of system development regulated by the functional safety standard ISO 26262.

The concrete project outcomes will be (i) a language by which requirements can be formalised and related to the system architecture, (ii) methods for automatic verification of architectural models against requirements, and (iii) a prototype implementation of the developed framework compatible with the industrial practices and processes.

From an industrial perspective, the adoption of these new methods and techniques raises challenges concerning the integration of new practices and related tools in the industrial processes and tool-chains.  In order to tackle this problem, VeriSpec seeks for close interaction between academia (MDH) and industry (Scania CV and AB Volvo).

[Show all publications]

Statistical Model Checking of Complex Robotic Systems (Oct 2019)
Mohammed Foughali , Félix Ingrand , Cristina Seceleanu
26th International Symposium on Model Checking of Software (SPIN 2019)

Optimized Allocation of Fault-tolerant Embedded Software with End-to-end Timing Constraints (May 2019)
Nesredin Mahmud, Cristina Seceleanu, Hamid Reza Faragardi, Guillermo Rodriguez-Navas, Saad Mubeen

Specifying Industrial System Requirements using Specification Patterns: A Case Study of Evaluation with Practitioners (May 2019)
Predrag Filipovikj, Cristina Seceleanu
14th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2019)

Bounded Invariance Checking of Simulink Models (Apr 2019)
Predrag Filipovikj, Guillermo Rodriguez-Navas, Cristina Seceleanu
The 34th ACM/SIGAPP Symposium On Applied Computing (SAC'19)

Bounded Verification of Simulink Models (Dec 2018)
Predrag Filipovikj, Guillermo Rodriguez-Navas, Cristina Seceleanu

Power-aware Allocation of Fault-tolerant Multi-rate AUTOSAR Applications (Dec 2018)
Nesredin Mahmud, Guillermo Rodriguez-Navas, Hamid Reza Faragardi, Saad Mubeen, Cristina Seceleanu
25th Asia-Pacific Software Engineering Conference (APSEC'18)