Paper Info
Title
Applying Parametric Model-Checking Techniques for Reusing Real-Time Critical Systems.
Abstract
Due to the increase of complexity in real-time safety-critical systems, verification and validation costs have significantly increased. A straightforward way to reduce costs is to reuse existing systems, adapting them to new requirements, so as to avoid new costly developments. Our aim is to verify during the development strategy definition phase whether the existing products can be reused and adapted for a new customer, by identifying key parameters to be tuned in order to reuse existing products. Performing efficient verification is therefore crucial. In this paper, we focus on the performance requirement aspects. Nowadays, model-checking techniques have improved significantly to verify the performances of real-time systems. However, model-checking cannot address real-time systems where some timing constants are unknown or uncertain. Parametric model-checking leverage this shortcoming by identifying parameter ranges for which the system is correct. We report here on an experiment of the evaluation of the use of these formal techniques applied to automatize the synthesis of good parameter ranges for system reuse in the setting of the environment requirements for an aerial video tracking system.
Year
DOI
Venue
2016
10.1007/978-3-319-53946-1_8
Communications in Computer and Information Science
Keywords
Field
DocType
Real-time systems,Safety-critical systems,Formal methods,Parametric verification,Performance verification,Case study,Avionics
Parametric model,Life-critical system,Verification and validation,Reuse,Computer science,Avionics,Formal methods,Reliability engineering,Time critical
Conference
Volume
ISSN
Citations 
694
1865-0929
0
PageRank 
References 
Authors
0.34
0
7
Name
Order
Citations
PageRank
Baptiste Parquier100.34
Laurent Rioux241.54
Rafik Henia316113.71
Romain Soulat4786.50
olivier h roux567146.30
didier lime678746.02
Étienne André729435.08