ST-Lib: A Library for Specifying and Classifying Model Behaviors
ST-Lib: A Library for Specifying and Classifying Model Behaviors
复制标题
ST-Lib：用于指定和分类模型行为的库
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
S. Seshia
中科院分区：
文献类型：
--
作者：
J. Kapinski;Xiaoqing Jin;Jyotirmoy V. Deshmukh;Alexandre Donzé;Tomoya Yamaguchi;Hisahiro Ito;T. Kaga;Shunsuke Kobuna;S. Seshia
测试和验证程序是汽车领域嵌入式控制系统开发过程的重要方面。形式化需求可用于自动化程序中，以检查仿真或实验结果是否符合设计规范，甚至对设计模型进行自动测试和形式化验证；然而，开发正式需求通常需要控制软件设计人员投入大量时间和精力。我们提出信号模板库（ST-Lib），这是一种统一的建模语言，以正式的需求语言封装许多有用的信号模式，目的是促进汽车控制应用的需求制定。 ST-Lib 由称为信号模板的基本模块组成。非正式地，它们指定特征信号形状并提供数值参数来调整形状。我们为 ST-Lib 提出了两个用例：(1) 允许设计人员根据用户定义的信号模板数值参数对设计行为进行分类，(2) 自动识别嵌入式控制系统给定闭环模型的信号模板参数的最坏情况值。我们通过两个案例研究证明 ST-Lib 的有效性，展示如何使用 ST-Lib 来提高用户工作效率。
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.