Reference : Trace-Checking Signal-based Temporal Properties: A Model-Driven Approach

	Document type :	Scientific congresses, symposiums and conference proceedings : Paper published in a book
	Discipline(s) :	Engineering, computing & technology : Computer science
	Focus Areas :	Security, Reliability and Trust
	To cite this reference:	http://hdl.handle.net/10993/44159

Title :	Trace-Checking Signal-based Temporal Properties: A Model-Driven Approach
Language :	English
Author, co-author :	Boufaied, Chaima [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
	Menghi, Claudio [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
	Bianculli, Domenico [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
	Briand, Lionel [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
	Isasi Parache, Yago []
Publication date :	Sep-2020
Main document title :	Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering (ASE ’20)
Peer reviewed :	Yes
On invitation :	No
Audience :	International
Event name :	35th IEEE/ACM International Conference on Automated Software Engineering (ASE ’20)
Event date :	from 21-09-2020 to 25-09-2020
Keywords :	[en] trace checking ; run-time verification ; temporal properties ; specification patterns ; model-driven ; cyber-physical systems ; signals
Abstract :	[en] Signal-based temporal properties (SBTPs) characterize the behavior of a system when its inputs and outputs are signals over time; they are very common for the requirements specification of cyber-physical systems. Although there exist several specification languages for expressing SBTPs, such languages either do not easily allow the specification of important types of properties (such as spike or oscillatory behaviors), or are not supported by (efficient) trace-checking procedures. In this paper, we propose SB-TemPsy, a novel model-driven trace-checking approach for SBTPs. SB-TemPsy provides (i) SB-TemPsy-DSL, a domain-specific language that allows the specification of SBTPs covering the most frequent requirement types in cyber-physical systems, and (ii) SB-TemPsy-Check, an efficient, model-driven trace-checking procedure. This procedure reduces the problem of checking an SB-TemPsy-DSL property over an execution trace to the problem of evaluating an Object Constraint Language constraint on a model of the execution trace. We evaluated our contributions by assessing the expressiveness of SB-TemPsy-DSL and the applicability of SB-TemPsy-Check using a representative industrial case study in the satellite domain. SB-TemPsy-DSL could express 97% of the requirements of our case study and SB-TemPsy-Check yielded a trace-checking verdict in 87% of the cases, with an average checking time of 48.7 s. From a practical standpoint and compared to state-of-the-art alternatives, our approach strikes a better trade-off between expressiveness and performance as it supports a large set of property types that can be checked, in most cases, within practical time limits.
Research centres :	Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab) ; University of Luxembourg: High Performance Computing - ULHPC
Funders :	European Commission - EC ; University of Luxembourg - UL
Name of the research project :	R-AGR-0731-00
Target :	Researchers ; Professionals
Permalink :	http://hdl.handle.net/10993/44159
Framework Programme / European Project :	H2020 ; 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems

	File(s) associated to this reference
	Fulltext file(s): File Commentary Version Size Access Open access ase2020.pdf Author postprint 1.25 MB View/Open

All documents in ORBi^lu are protected by a user license.

 

University of Luxembourg Library |  Feedback |  Legal notices Site Map