You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.
The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.
For the reports in this repository we specifically note that
- the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at http://www.ieee.org/web/publications/rights/copyrightpolicy.html)
- the use of articles under ACM copyright is governed by the ACM copyright policy (available at http://www.acm.org/pubs/copyright_policy/)
- technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
- in other cases, please contact the copyright owner for detailed information
By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.
If you are in doubt, feel free to contact webmaster@ide.mdh.se
Using Safety Analysis Techniques To Derive Safety Properties For Formal Verification Of Safety-Critical Systems
Authors:
Ermia Hassanpour
Publication Type:
Master Theses
Abstract
Failure of safety-critical systems may cause severe injury to humans or the environment. In
order to ensure the safety of such systems, rigorous methods must be used. Formal verification
is one of these methods that helps in ensuring the system safety based on robust mathematical
methods. Formal verification helps to prove certain properties of the model. This mathematical
proof can strengthen the evidence for the safety claims of the system and help in standardization
and receiving certificates. Defining safety properties for formal verification, more specifically for
model checking, is very challenging. Finding the right set of properties, and writing these properties
as temporal logic formulas, are difficult tasks for safety experts, software engineers, and developers.
Model-driven development utilizes the concept of abstraction to deal with the complexity of systems
and allow for earlier safety analysis. In this thesis, we intend to use model-driven methods and
their supporting safety analysis tools to help in deriving the safety properties for model checking.
We use Timed Rebeca language and Afra model checking tool for formal verification, and CHESS
tools for modelling the system and for safety analysis. As part of CHESS, ConcertoFLA technique
includes the combination and automation of traditional safety analysis techniques that provide a
qualitative assessment of the dependability of component-based systems. Failure Propagation Trans-
form Calculus (FPTC) rules are the result of ConcertoFLA analysis. We extract safety contracts
from FPTC rules. Then, we introduce a mapping between safety contracts and temporal logic prop-
erties in Afra. We also map internal block diagrams and sequence diagrams from CHESS models
to Rebeca models to be able to perform model checking. Furthermore, we applied our approach to
two case studies and used safety analysis results to more effectively derive the safety properties,
and model check and debug the models.
Bibtex
@misc{Hassanpour6879,
author = {Ermia Hassanpour},
title = {Using Safety Analysis Techniques To Derive Safety Properties For Formal Verification Of Safety-Critical Systems},
month = {October},
year = {2022},
url = {http://www.es.mdu.se/publications/6879-}
}
