Specification and Validation of a Real-Time Parallel Kernel using LOTOS

Cléver Guareis de farias; Luis Ferreira Pires; Wanderley Lopes de Souza; Célio Estevan Moron

doi:10.1109/MASCOT.2001.948848

Specification and Validation of a Real-Time Parallel Kernel using LOTOS

Cléver Guareis de farias, Luis Ferreira Pires, Wanderley Lopes de Souza, Célio Estevan Moron

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

133 Downloads (Pure)

Abstract

This paper presents and discusses the LOTOS specification of a real-time parallel kernel. The purpose of this specification exercise has been to evaluate LOTOS with respect to its capabilities to model real-time features with a realistic industrial product. LOTOS was used to produce the formal specification of TRANS-RTXC, which is a real-time parallel kernel developed by Intelligent Systems International. This paper shows that although timing constraints cannot be explicitly represented in LOTOS, the language is suitable for the specification of co-ordination of real-time tasks, which is the main functionality of the real-time kernel. This paper also discusses the validation process of the kernel specification and the role of tools in this validation process. We believe that our experience (use of structuring techniques, use of validation methods and tools, etc.) is valuable for designers who want to apply formal models in their design or analysis tasks

Original language	English
Title of host publication	MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems
Editors	S.R. Das, D. Nicol, F. Perrone
Publisher	University of Cincinatti
Pages	7-14
Number of pages	8
ISBN (Print)	0-7695-1315-8
DOIs	https://doi.org/10.1109/MASCOT.2001.948848
Publication status	Published - 15 Aug 2001
Event	9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS 2001 - Cincinatti, United States Duration: 15 Aug 2001 → 18 Aug 2001 Conference number: 9

Conference

Conference	9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS 2001
Abbreviated title	MASCOTS
Country/Territory	United States
City	Cincinatti
Period	15/08/01 → 18/08/01

Keywords

METIS-204031
IR-37117

Access to Document

10.1109/MASCOT.2001.948848

00000066Accepted author version, 107 KB

Cite this

Guareis de farias, C., Ferreira Pires, L., Lopes de Souza, W., & Moron, C. E. (2001). Specification and Validation of a Real-Time Parallel Kernel using LOTOS. In S. R. Das, D. Nicol, & F. Perrone (Eds.), MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (pp. 7-14). University of Cincinatti. https://doi.org/10.1109/MASCOT.2001.948848

Guareis de farias, Cléver ; Ferreira Pires, Luis ; Lopes de Souza, Wanderley et al. / Specification and Validation of a Real-Time Parallel Kernel using LOTOS. MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. editor / S.R. Das ; D. Nicol ; F. Perrone. University of Cincinatti, 2001. pp. 7-14

@inproceedings{27da68e77b4a4d00bfe61474767db4be,

title = "Specification and Validation of a Real-Time Parallel Kernel using LOTOS",

abstract = "This paper presents and discusses the LOTOS specification of a real-time parallel kernel. The purpose of this specification exercise has been to evaluate LOTOS with respect to its capabilities to model real-time features with a realistic industrial product. LOTOS was used to produce the formal specification of TRANS-RTXC, which is a real-time parallel kernel developed by Intelligent Systems International. This paper shows that although timing constraints cannot be explicitly represented in LOTOS, the language is suitable for the specification of co-ordination of real-time tasks, which is the main functionality of the real-time kernel. This paper also discusses the validation process of the kernel specification and the role of tools in this validation process. We believe that our experience (use of structuring techniques, use of validation methods and tools, etc.) is valuable for designers who want to apply formal models in their design or analysis tasks",

keywords = "METIS-204031, IR-37117",

author = "{Guareis de farias}, Cl{\'e}ver and {Ferreira Pires}, Luis and {Lopes de Souza}, Wanderley and Moron, {C{\'e}lio Estevan}",

year = "2001",

month = aug,

day = "15",

doi = "10.1109/MASCOT.2001.948848",

language = "English",

isbn = "0-7695-1315-8",

pages = "7--14",

editor = "S.R. Das and D. Nicol and F. Perrone",

booktitle = "MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems",

publisher = "University of Cincinatti",

note = "9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS 2001, MASCOTS ; Conference date: 15-08-2001 Through 18-08-2001",

}

Guareis de farias, C, Ferreira Pires, L, Lopes de Souza, W & Moron, CE 2001, Specification and Validation of a Real-Time Parallel Kernel using LOTOS. in SR Das, D Nicol & F Perrone (eds), MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. University of Cincinatti, pp. 7-14, 9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS 2001, Cincinatti, Ohio, United States, 15/08/01. https://doi.org/10.1109/MASCOT.2001.948848

Specification and Validation of a Real-Time Parallel Kernel using LOTOS. / Guareis de farias, Cléver; Ferreira Pires, Luis; Lopes de Souza, Wanderley et al.
MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. ed. / S.R. Das; D. Nicol; F. Perrone. University of Cincinatti, 2001. p. 7-14.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Specification and Validation of a Real-Time Parallel Kernel using LOTOS

AU - Guareis de farias, Cléver

AU - Ferreira Pires, Luis

AU - Lopes de Souza, Wanderley

AU - Moron, Célio Estevan

N1 - Conference code: 9

PY - 2001/8/15

Y1 - 2001/8/15

N2 - This paper presents and discusses the LOTOS specification of a real-time parallel kernel. The purpose of this specification exercise has been to evaluate LOTOS with respect to its capabilities to model real-time features with a realistic industrial product. LOTOS was used to produce the formal specification of TRANS-RTXC, which is a real-time parallel kernel developed by Intelligent Systems International. This paper shows that although timing constraints cannot be explicitly represented in LOTOS, the language is suitable for the specification of co-ordination of real-time tasks, which is the main functionality of the real-time kernel. This paper also discusses the validation process of the kernel specification and the role of tools in this validation process. We believe that our experience (use of structuring techniques, use of validation methods and tools, etc.) is valuable for designers who want to apply formal models in their design or analysis tasks

AB - This paper presents and discusses the LOTOS specification of a real-time parallel kernel. The purpose of this specification exercise has been to evaluate LOTOS with respect to its capabilities to model real-time features with a realistic industrial product. LOTOS was used to produce the formal specification of TRANS-RTXC, which is a real-time parallel kernel developed by Intelligent Systems International. This paper shows that although timing constraints cannot be explicitly represented in LOTOS, the language is suitable for the specification of co-ordination of real-time tasks, which is the main functionality of the real-time kernel. This paper also discusses the validation process of the kernel specification and the role of tools in this validation process. We believe that our experience (use of structuring techniques, use of validation methods and tools, etc.) is valuable for designers who want to apply formal models in their design or analysis tasks

KW - METIS-204031

KW - IR-37117

U2 - 10.1109/MASCOT.2001.948848

DO - 10.1109/MASCOT.2001.948848

M3 - Conference contribution

SN - 0-7695-1315-8

SP - 7

EP - 14

BT - MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems

A2 - Das, S.R.

A2 - Nicol, D.

A2 - Perrone, F.

PB - University of Cincinatti

T2 - 9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS 2001

Y2 - 15 August 2001 through 18 August 2001

ER -

Guareis de farias C, Ferreira Pires L, Lopes de Souza W, Moron CE. Specification and Validation of a Real-Time Parallel Kernel using LOTOS. In Das SR, Nicol D, Perrone F, editors, MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. University of Cincinatti. 2001. p. 7-14 doi: 10.1109/MASCOT.2001.948848

Specification and Validation of a Real-Time Parallel Kernel using LOTOS

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this