The search functionality is under construction.

The search functionality is under construction.

Because processes run concurrently in multitask systems, the size of the state space grows exponentially. Therefore, it is not straightforward to formally verify that such systems enjoy desired properties. Real-time constrains make the formal verification more challenging. In this paper, we propose the following to address the challenge: (1) a way to model multitask real-time systems as observational transition systems (OTSs), a kind of state transition systems, (2) a way to describe their specifications in CafeOBJ, an algebraic specification language, and (3) a way to verify that such systems enjoy desired properties based on such formal specifications by writing proof scores, proof plans, in CafeOBJ. As a case study, we model Fischer's protocol, a well-known real-time mutual exclusion protocol, as an OTS, describe its specification in CafeOBJ, and verify that the protocol enjoys the mutual exclusion property when an arbitrary number of processes participates in the protocol^{*}.

- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E105-A No.5 pp.823-832

- Publication Date
- 2022/05/01

- Publicized
- 2021/09/24

- Online ISSN
- 1745-1337

- DOI
- 10.1587/transfun.2021MAP0007

- Type of Manuscript
- Special Section PAPER (Special Section on Mathematical Systems Science and its Applications)

- Category

Masaki NAKAMURA

Toyama Prefectural University

Shuki HIGASHI

Toyama Prefectural University,Hokuden Information System Service Company, Inc.

Kazutoshi SAKAKIBARA

Toyama Prefectural University

Kazuhiro OGATA

Japan Advanced Institute of Science and Technology

The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.

Copy

Masaki NAKAMURA, Shuki HIGASHI, Kazutoshi SAKAKIBARA, Kazuhiro OGATA, "Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method" in IEICE TRANSACTIONS on Fundamentals,
vol. E105-A, no. 5, pp. 823-832, May 2022, doi: 10.1587/transfun.2021MAP0007.

Abstract: Because processes run concurrently in multitask systems, the size of the state space grows exponentially. Therefore, it is not straightforward to formally verify that such systems enjoy desired properties. Real-time constrains make the formal verification more challenging. In this paper, we propose the following to address the challenge: (1) a way to model multitask real-time systems as observational transition systems (OTSs), a kind of state transition systems, (2) a way to describe their specifications in CafeOBJ, an algebraic specification language, and (3) a way to verify that such systems enjoy desired properties based on such formal specifications by writing proof scores, proof plans, in CafeOBJ. As a case study, we model Fischer's protocol, a well-known real-time mutual exclusion protocol, as an OTS, describe its specification in CafeOBJ, and verify that the protocol enjoys the mutual exclusion property when an arbitrary number of processes participates in the protocol^{*}.

URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.2021MAP0007/_p

Copy

@ARTICLE{e105-a_5_823,

author={Masaki NAKAMURA, Shuki HIGASHI, Kazutoshi SAKAKIBARA, Kazuhiro OGATA, },

journal={IEICE TRANSACTIONS on Fundamentals},

title={Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method},

year={2022},

volume={E105-A},

number={5},

pages={823-832},

abstract={Because processes run concurrently in multitask systems, the size of the state space grows exponentially. Therefore, it is not straightforward to formally verify that such systems enjoy desired properties. Real-time constrains make the formal verification more challenging. In this paper, we propose the following to address the challenge: (1) a way to model multitask real-time systems as observational transition systems (OTSs), a kind of state transition systems, (2) a way to describe their specifications in CafeOBJ, an algebraic specification language, and (3) a way to verify that such systems enjoy desired properties based on such formal specifications by writing proof scores, proof plans, in CafeOBJ. As a case study, we model Fischer's protocol, a well-known real-time mutual exclusion protocol, as an OTS, describe its specification in CafeOBJ, and verify that the protocol enjoys the mutual exclusion property when an arbitrary number of processes participates in the protocol^{*}.},

keywords={},

doi={10.1587/transfun.2021MAP0007},

ISSN={1745-1337},

month={May},}

Copy

TY - JOUR

TI - Specification and Verification of Multitask Real-Time Systems Using the OTS/CafeOBJ Method

T2 - IEICE TRANSACTIONS on Fundamentals

SP - 823

EP - 832

AU - Masaki NAKAMURA

AU - Shuki HIGASHI

AU - Kazutoshi SAKAKIBARA

AU - Kazuhiro OGATA

PY - 2022

DO - 10.1587/transfun.2021MAP0007

JO - IEICE TRANSACTIONS on Fundamentals

SN - 1745-1337

VL - E105-A

IS - 5

JA - IEICE TRANSACTIONS on Fundamentals

Y1 - May 2022

AB - Because processes run concurrently in multitask systems, the size of the state space grows exponentially. Therefore, it is not straightforward to formally verify that such systems enjoy desired properties. Real-time constrains make the formal verification more challenging. In this paper, we propose the following to address the challenge: (1) a way to model multitask real-time systems as observational transition systems (OTSs), a kind of state transition systems, (2) a way to describe their specifications in CafeOBJ, an algebraic specification language, and (3) a way to verify that such systems enjoy desired properties based on such formal specifications by writing proof scores, proof plans, in CafeOBJ. As a case study, we model Fischer's protocol, a well-known real-time mutual exclusion protocol, as an OTS, describe its specification in CafeOBJ, and verify that the protocol enjoys the mutual exclusion property when an arbitrary number of processes participates in the protocol^{*}.

ER -