A spiral process of formalization and verification: A case study on verification of the scheduling mechanism of OSEK/VDX
A spiral process of formalization and verification: A case study on verification of the scheduling mechanism of OSEK/VDX
复制标题
形式化与验证的螺旋式过程：以OSEK/VDX调度机制验证为例
DOI：
10.1016/j.jisa.2016.05.002
复制
发表时间：
2016-12
影响因子：
5.6
通讯作者：
Yueying He
中科院分区：
文献类型：
--
作者：
Min Zhang;Toshiaki Aoki;Yueying He
由于软件系统的复杂性不断增加，系统的形式化和验证通常不是一次性的任务。形式化和验证之间的关系不应该是顺序的，而是迭代的，因为验证在形式化之后，反过来帮助验证和细化形式化。迭代是一个螺旋式的过程，一个正式的模型被逐步开发，更多的属性被验证。在本文中，我们提出了这样一个螺旋过程中做形式化和验证的具体案例研究，以展示我们如何形式化和验证的螺旋方式的调度机制和优先级上限协议（PCP）的工业汽车标准称为OSEK/VDX。我们选择了一个代数形式化语言CafeOBJ的模块化和交互式定理证明功能的特点。我们从调度机制的原型模型开始，根据验证结果对其进行验证和改进。通过定理证明，它加强了我们对规范及其与指定问题域之间的差距的理解。形式模型被细化，直到所有这些属性被成功证明。我们逐步扩展它的形式化PCP和验证更多的属性，如死锁自由和优先级反转自由。
Formalization and verification of a system usually are not one time tasks due to the increasing complexity of software systems. The relation between formalization and verification should not be sequential but iterative in that verification follows formalization and in turn helps validate and refine formalization. The iteration is a spiral process with a formal model being incrementally developed and more properties being verified. In this paper, we present such a spiral process of doing formalization and verification with a concrete case study to demonstrate how we formalize and verify in the spiral manner a scheduling mechanism and Priority Ceiling Protocol (PCP) of an industrial automobile standard called OSEK/VDX. We choose an algebraic formal language called CafeOBJ for its features of modularity and interactive theorem proving functionality. We start with a prototypical model of the scheduling mechanism, validate and refine it based on verification results. By theorem proving, it reinforces our understanding of the specifications and their gap with the specified problem domains. The formal model is refined until all these properties are successfully proved. We incrementally extend it to formalize PCP and verify more properties such as deadlock freedom and priority inversion freedom.
登录
查看更多内容
DOI：
--
发表时间：
2003
期刊：
--
影响因子：
--
作者：
C. Doungsa-ard;T. Suwannasart
通讯作者：
C. Doungsa-ard;T. Suwannasart
DOI：
10.1016/j.tcs.2012.07.041
发表时间：
2012-12
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
K. Futatsugi;Daniel Găină;K. Ogata
通讯作者：
K. Futatsugi;Daniel Găină;K. Ogata
DOI：
10.1016/b978-044450813-3/50026-6
发表时间：
2001
期刊：
--
影响因子：
--
作者：
E. Clarke;Holger Schlingloff
通讯作者：
E. Clarke;Holger Schlingloff
DOI：
10.1007/978-3-642-61455-2_16
发表时间：
1996-09
期刊：
--
影响因子：
--
作者：
Edmund M. Clarke;O. Grumberg;D. E. Long
通讯作者：
Edmund M. Clarke;O. Grumberg;D. E. Long
DOI：
10.1109/real.2000.896005
发表时间：
2000-11
期刊：
Proceedings 21st IEEE Real-Time Systems Symposium
影响因子：
--
作者：
B. Dutertre
通讯作者：
B. Dutertre