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

C.R.G. de farias; L.F. Pires; W. de Souza; C.E. Moron

doi:10.1109/MASCOT.2001.948848

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

C.R.G. de farias
, L.F. Pires
, W. de Souza
, C.E. Moron

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

177 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
Subtitle of host publication	Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems
Editors	S.R. Das, D. Nicol, F. Perrone
Place of Publication	Piscataway, NJ
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

Publication series

Name	MASCOTS, Proceedings International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems
Publisher	IEEE
Number	9
Volume	2001
ISSN (Print)	1526-7639

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

Access to Document

10.1109/MASCOT.2001.948848

ArticleAccepted author version, 107 KB

1 Report

Specification and Validation of a Real-Time Parallel Kernel using LOTOS
Guareis de farias, C., Ferreira Pires, L., Lopes de Souza, W. & Estevan Moron, C., Jul 2001, Enschede: Centre for Telematics and Information Technology (CTIT). (CTIT technical report series; no. TR-CTIT-01-30)
Research output: Book/Report › Report › Other research output

Open Access
File

Cite this

de farias, C. R. G., Pires, L. F., 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). (MASCOTS, Proceedings International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems; Vol. 2001, No. 9). University of Cincinatti. https://doi.org/10.1109/MASCOT.2001.948848

de farias, C.R.G. ; Pires, L.F. ; de Souza, W. 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. Piscataway, NJ : University of Cincinatti, 2001. pp. 7-14 (MASCOTS, Proceedings International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems; 9).

@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",

author = "\{de farias\}, C.R.G. and L.F. Pires and \{de Souza\}, W. and C.E. Moron",

year = "2001",

month = aug,

day = "15",

doi = "10.1109/MASCOT.2001.948848",

language = "English",

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

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

publisher = "University of Cincinatti",

number = "9",

pages = "7--14",

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

booktitle = "MASCOTS 2001",

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",

}

de farias, CRG, Pires, LF , 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. MASCOTS, Proceedings International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, no. 9, vol. 2001, University of Cincinatti, Piscataway, NJ, 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. / de farias, C.R.G.; Pires, L.F.; de Souza, W. 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. Piscataway, NJ: University of Cincinatti, 2001. p. 7-14 (MASCOTS, Proceedings International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems; Vol. 2001, No. 9).

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 - de farias, C.R.G.

AU - Pires, L.F.

AU - de Souza, W.

AU - Moron, C.E.

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

U2 - 10.1109/MASCOT.2001.948848

DO - 10.1109/MASCOT.2001.948848

M3 - Conference contribution

SN - 0-7695-1315-8

T3 - MASCOTS, Proceedings International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems

SP - 7

EP - 14

BT - MASCOTS 2001

A2 - Das, S.R.

A2 - Nicol, D.

A2 - Perrone, F.

PB - University of Cincinatti

CY - Piscataway, NJ

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 -

de farias CRG, Pires LF , 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. Piscataway, NJ: University of Cincinatti. 2001. p. 7-14. (MASCOTS, Proceedings International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems; 9). doi: 10.1109/MASCOT.2001.948848

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

Abstract

Publication series

Conference

Access to Document

Fingerprint

Research output

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

Cite this