AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic
- PDF / 2,359,786 Bytes
- 18 Pages / 595.276 x 790.866 pts Page_size
- 28 Downloads / 158 Views
STTT Special Issue TACAS 2018
AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic Dejan Niˇckovi´c1 · Olivier Lebeltel2 · Oded Maler2 · Thomas Ferrère3 · Dogan Ulus4
© Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract We introduce in this paper AMT 2.0, a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended signal temporal logic, which integrates timed regular expressions within signal temporal logic. The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal. We demonstrate the tool functionality on several running examples and case studies, and evaluate its performance. Keywords Runtime verification · Monitoring · Trace diagnostics · Property measuring · Temporal logic
1 Introduction Cyber-physical systems, such as automotive embedded controllers, medical devices or autonomous vehicles, are often modeled and analyzed by simulation. Simulators generate traces admitting real values often interpreted as continuoustime signals. To evaluate the system under design, these traces are inspected for satisfying some correctness requirements and are often subject to quantitative analysis based on recording some values in certain segments of the signal and performing some computation (summation, minimum) on them. Over the past decade, an extensive framework has been developed whose goal was to bring automated support for this tedious and error-prone task, centered around signal temporal logic (STL) [19,20]. STL extends the classical LTL in two directions: It uses predicates over real-valued variables in addition to atomic propositions, and it is defined over dense
B
Dejan Niˇckovi´c [email protected]
1
AIT Austrian Institute of Technology, Seibersdorf, Austria
2
Verimag, CNRS/University of Grenoble-Alpes, Grenoble, France
3
IST Austria, Klosterneuburg, Austria
4
Boston University, Boston, USA
continuous time accessed symbolically with timed modalities as in metric temporal logic (MTL) [18]. This framework, which was initially accompanied by a rudimentary prototype tool [23], had a lot of reported applications in domains such as automotive, robotics, analog circuits, systems biology. It can be viewed as an extension of runtime verification toward cyber-physical hybrid systems. Interested readers may consult the survey in [6]. In this article, we present AMT 2.0, a new version of the tool. The new version is much more mature in terms of software engineering aspects such as rigorous typing of signals and properties, introducing programming language features that include declarations and aliases, improvement of the graphical editors, systematic software testing, etc. Furthermore, its functionality has been extended signi
Data Loading...
