Reference : Specifying Source Code and Signal-based Behaviour of CPS Components

	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/52185

Title :	Specifying Source Code and Signal-based Behaviour of CPS Components
Language :	English
Author, co-author :	Dawes, Joshua [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
	Bianculli, Domenico [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV >]
Publication date :	Nov-2022
Main document title :	Proceedings of the 18th International Conference on Formal Aspects of Component Software
Author, co-author :	Dawes, Joshua
	Bianculli, Domenico
Publisher :	Springer
Peer reviewed :	Yes
On invitation :	No
Audience :	International
Event name :	18th International Conference on Formal Aspects of Component Software
Event date :	from 10-11-2022 to 11-11-2022
Event place (city) :	Virtual
Keywords :	[en] specification language ; temporal logic ; cyber-physical systems
Abstract :	[en] Specifying properties over the behaviour of components of Cyber-Physical Systems usually focuses on the behaviour of signals, i.e., the behaviour of the physical part of the system, leaving the behaviour of the cyber components implicit. There have been some attempts to provide specification languages that enable more explicit reference to the behaviour of cyber components, but it remains awkward to directly express the behaviour of both cyber and physical components in the same specification, using one formalism. In this paper, we introduce a new specification language, Source Code and Signal Logic (SCSL), that 1) provides syntax specific to both signals and events originating in source code; and 2) does not require source code events to be abstracted into signals. We introduce SCSL by giving its syntax and semantics, along with examples. We then provide a comparison between SCSL and existing specification languages, using an example property, to show the benefit of using SCSL to capture certain types of properties.
Research centres :	Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)
Funders :	European Commission - EC
Target :	Researchers ; Professionals
Permalink :	http://hdl.handle.net/10993/52185
Framework Programme / European Project :	H2020 ; 957254 - COSMOS - DevOps for Complex Cyber-Physical Systems

	File(s) associated to this reference
	Fulltext file(s): File Commentary Version Size Access Open access camera-ready.pdf Camera-ready Author postprint 293.93 kB View/Open Open access extended.pdf Extended version, with appendices. Author postprint 322.26 kB View/Open

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

 

University of Luxembourg Library |  Feedback |  Legal notices Site Map