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


Share/Save/Bookmark

Guareis de Farias, C.R. and Ferreira Pires, L. and Lopes de Souza, W. and Moron, C.M. (2001) Specification and Validation of a Real-Time Parallel Kernel Using LOTOS. In: 9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 2001), 15-18 Aug 2001, Cincinatti, Ohio, U.S.A. (pp. pp. 7-14).

open access
[img]
Preview
PDF
102kB
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.
Item Type:Conference or Workshop Item
Additional information:Imported from research group ASNA (ID number 151)
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/66756
Official URL:http://dx.doi.org/10.1109/MASCOT.2001.948848
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page