Trace-Checking Signal-based Temporal Properties: A Model-Driven Approach
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.
Thu 24 SepDisplayed time zone: (UTC) Coordinated Universal Time change
08:00 - 09:00
Model-Driven Development and Rapid PrototypingTool Demonstrations / Research Papers at Wombat
Chair(s): Timo Kehrer Humboldt-Universtität zu Berlin
|Scalable Multiple-View Analysis of Reactive Systems via Bidirectional Model Transformations|
Christos Tsigkanos TU Vienna, NIANYU LI Peking University, China, Zhi Jin Peking University, Zhenjiang Hu Peking University, China, Carlo Ghezzi Politecnico di Milano
|Trace-Checking Signal-based Temporal Properties: A Model-Driven Approach|
Chaima Boufaied University of Luxembourg, Claudio Menghi University of Luxembourg, Luxembourg, Domenico Bianculli University of Luxembourg, Lionel Briand SnT Centre/University of Luxembourg, Yago Isasi Parache LuxSpace
|GUI2WiRe: Rapid Wireframing with a Mined and Large-Scale GUI Repository using Natural Language Requirements|
Kristian Kolthoff Institute for Enterprise Systems (InES), University Of Mannheim, Christian Bartelt Institute for Software and Systems Engineering, TU Clausthal, Simone Paolo Ponzetto Data and Web Science Group, University of Mannheim