TY - GEN
T1 - A Spiral Proceb of Modeling and Verifying the Scheduling Mechanism of OSEK/VDX in OTS/CafeOBJ Method
AU - Zhang, Min
AU - Aoki, Toshiaki
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2016/3/15
Y1 - 2016/3/15
N2 - Formalization and verification of a system usually are not one time tasks, particularly when the system to be formalized and verified is complicated. 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 proceb with a formal model being incrementally developed and more and more properties being verified. In this paper, we present a case study to demonstrate how we formalize and verify in the spiral way a scheduling mechanism and Priority Ceiling Protocol of an industrial automobile standard, i.e. OSEK/VDX, in OTS/CafeOBJ method, an algebraic approach to modeling and verifying systems by interactive theorem proving in CafeOBJ. We start with a prototypical model of the scheduling mechanism, validate and refine it based on verification results. By theorem proving, it reinforces the specifier's understanding of the specifications and their relationship with the specified problem domains. The formal model is refined until all these properties are succebfully proved. We then incrementally extend it to cover more complicated part and verify more properties such as exclusion, deadlock freedom, priority inversion freedom.
AB - Formalization and verification of a system usually are not one time tasks, particularly when the system to be formalized and verified is complicated. 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 proceb with a formal model being incrementally developed and more and more properties being verified. In this paper, we present a case study to demonstrate how we formalize and verify in the spiral way a scheduling mechanism and Priority Ceiling Protocol of an industrial automobile standard, i.e. OSEK/VDX, in OTS/CafeOBJ method, an algebraic approach to modeling and verifying systems by interactive theorem proving in CafeOBJ. We start with a prototypical model of the scheduling mechanism, validate and refine it based on verification results. By theorem proving, it reinforces the specifier's understanding of the specifications and their relationship with the specified problem domains. The formal model is refined until all these properties are succebfully proved. We then incrementally extend it to cover more complicated part and verify more properties such as exclusion, deadlock freedom, priority inversion freedom.
KW - CafeOBJ
KW - OSEK/VDX standard
KW - OTS
KW - Theorem proving
UR - https://www.scopus.com/pages/publications/84966662658
U2 - 10.1109/DCIT.2015.18
DO - 10.1109/DCIT.2015.18
M3 - 会议稿件
AN - SCOPUS:84966662658
T3 - Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015
SP - 11
EP - 20
BT - Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015
Y2 - 16 November 2015 through 19 November 2015
ER -