- 【Updated on May 12, 2025】 Integration of CiNii Dissertations and CiNii Books into CiNii Research
- Trial version of CiNii Research Knowledge Graph Search feature is available on CiNii Labs
- 【Updated on June 30, 2025】Suspension and deletion of data provided by Nikkei BP
- Regarding the recording of “Research Data” and “Evidence Data”
Formal verification of Fischer’s real-time mutual exclusion protocol by the OTS/CafeOBJ method
Description
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.
Journal
-
- 2020 59th Annual Conference of the Society of Instrument and Control Engineers of Japan (SICE)
-
2020 59th Annual Conference of the Society of Instrument and Control Engineers of Japan (SICE) 1210-1215, 2020-09-23
IEEE
- Tweet
Details 詳細情報について
-
- CRID
- 1360576122904171264
-
- Data Source
-
- Crossref
- OpenAIRE