2020年9月23日
Formal verification of Fischer's real-time mutual exclusion protocol by the OTS/CafeOBJ method
2020 59th Annual Conference of the Society of Instrument and Control Engineers of Japan, SICE 2020
- ,
- ,
- ,
- 開始ページ
- 1210
- 終了ページ
- 1215
- 記述言語
- 掲載種別
- 研究論文(国際会議プロシーディングス)
- 出版者・発行元
- IEEE
Fischer's protocol is a well-known real-time mutual exclusion protocol for multiple processes. The mutual exclusiveness is guaranteed by treating time aspects of transitions. In such a multitask real-time system, since processes run concurrently, the size of the state space grows exponentially. It is not easy to verify time constraints of a give system. Formal descriptions of multitask real-time systems may help us to verify time constraints formally with computer supports. In this paper, as a case study of the OTS/CafeOBJ method, we model Fischer's protocol as an observational transition system, describe it in CafeOBJ algebraic specification language, and verify that different processes do not enter the critical section at the same time by the proof score method based on equational reasoning implemented in CafeOBJ interpreter.
- リンク情報
-
- DBLP
- https://dblp.uni-trier.de/rec/conf/sice/0001HSO20
- URL
- https://ieeexplore.ieee.org/document/9240272
- URL
- https://dblp.uni-trier.de/conf/sice/2020
- URL
- https://dblp.uni-trier.de/db/conf/sice/sice2020.html#0001HSO20
- Scopus
- https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85096355128&origin=inward
- Scopus Citedby
- https://www.scopus.com/inward/citedby.uri?partnerID=HzOxMe3b&scp=85096355128&origin=inward
- ID情報
-
- ISBN : 9781728110899
- DBLP ID : conf/sice/0001HSO20
- SCOPUS ID : 85096355128