ST-Lib: A Library for Specifying and Classifying Model Behaviors

James Kapinski, Xiaoqing Jin, Jyotirmoy Deshmukh, Alexandre Donze, Tomoya Yamaguchi, Hisahiro Ito, Tomoyuki Kaga, Shunsuke Kobuna, and Sanjit Seshia. ST-Lib: A Library for Specifying and Classifying Model Behaviors. In SAE World Congress and Exhibition, SAE Technical Paper 2016-01-0621, SAE International, April 2016.

Download

[HTML] 

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.

BibTeX

@inproceedings{kapinski-sae16,
 author="James Kapinski and Xiaoqing Jin and Jyotirmoy Deshmukh and Alexandre Donze and Tomoya Yamaguchi and Hisahiro Ito and Tomoyuki Kaga and Shunsuke Kobuna and Sanjit Seshia",
 publisher="SAE International",
 title="{ST-Lib}: A Library for Specifying and Classifying Model Behaviors", 
 booktitle="SAE World Congress and Exhibition, SAE Technical Paper 2016-01-0621",
 year="2016",
 month="April",
 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.",
}