This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
ST-Lib: A Library for Specifying and Classifying Model Behaviors
Technical Paper
2016-01-0621
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
Test and verification procedures are a vital aspect of the development process for embedded control systems in the automotive domain. Formal requirements can be used in automated procedures to check whether simulation or experimental results adhere to design specifications and even to perform automatic test and formal verification of design models; however, developing formal requirements typically requires significant investment of time and effort for control software designers. We propose Signal Template Library (ST-Lib), a uniform modeling language to encapsulate a number of useful signal patterns in a formal requirement language with the goal of facilitating requirement formulation for automotive control applications. ST-Lib consists of basic modules known as signal templates. Informally, these specify a characteristic signal shape and provide numerical parameters to tune the shape. We propose two use-cases for ST-Lib: (1) allowing designers to classify design behaviors based on user-defined numerical parameters for signal templates, and (2) automatic identification of worst-case values for the signal template parameters for a given closed-loop model of an embedded control system. We show how ST-Lib can be used to improve user productivity by demonstrating its effectiveness on two case studies.
Authors
Topic
Citation
Kapinski, J., Jin, X., Deshmukh, J., Donze, A. et al., "ST-Lib: A Library for Specifying and Classifying Model Behaviors," SAE Technical Paper 2016-01-0621, 2016, https://doi.org/10.4271/2016-01-0621.Also In
References
- Annapureddy Yashwanth S. R. , Liu Che , Fainekos Georgios E. , and Sankaranarayanan Sriram S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems Proc. of Tools and Algorithms for the Construction and Analysis of Systems 254 257 2011
- Donzé Alexandre Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems Proc. of Computer Aided Verification 167 170 2010
- Donzé Alexandre Breach toolbox http://www.eecs.berkeley.edu/∼donze/breach_page.html 2015
- Fainekos Georgios E. , Sankaranarayanan Sriram , Ueda Koichi , and Yazarel Hakan Verification of Automotive Control Applications using S-TaLiRo Proc. of the American Control Conference 2012
- Sankaranarayanan Sriram Fainekos Georgios S-taliro toolbox https://sites.google.com/a/asu.edu/s-taliro/s-taliro 2015
- Jin Xiaoqing , Deshmukh Jyotirmoy V , Kapinski James , Ueda Koichi , and Butts Ken Powertrain control verification benchmark Proceedings of the 17th international conference on Hybrid systems: computation and control 253 262 ACM 2014
- Koymans R. Specifying real-time properties with metric temporal logic Real-Time Syst. 2 4 255 299 1990
- Maler Oded and Nickovic Dejan Monitoring Temporal Properties of Continuous Signals Proc. of Formal Modeling and Analysis of Timed Systems/ Formal Techniques in Real-Time and Fault Tolerant Systems 152 166 2004
- Nicolescu Gabriela and Mosterman Pieter J Model-based design for embedded systems CRC Press 2009
- Pnueli A. The Temporal Logic of Programs Proc. of Foundations of Computer Science 46 57 1977
- Wing Jeannette M A specifier’s introduction to formal methods Computer 23 9 8 22 1990