Title :
Schedulability and safety analysis in the graphical communicating shared resources
Author :
Ben-Abdallah, Hanene ; Young Si Kim ; Lee, Inkyu
Author_Institution :
Dept. of Comput. & Inf. Sci., Pennsylvania Univ., Philadelphia, PA
Abstract :
Graphical Communicating Shared Resources is a formal language for the specification and analysis of real-time systems, including their functional, temporal and resource requirements. GCSR supports the explicit representation of system resources and priorities to arbitrate resource contentions. These features allow a designer to examine resource inherent constraints and to experiment with various resource allocations and scheduling disciplines in order to produce a more dependable specification. In addition, GCSR has a precise operational semantics and notions of equivalence that allow the execution and formal analysis of a specification. In this paper, we show how to model a scheduling discipline and verify schedulability and safety properties within GCSR. We illustrate our method through a mobile robotic application
Keywords :
calculus of communicating systems; formal specification; real-time systems; resource allocation; scheduling; specification languages; state-space methods; formal analysis; formal language; functional requirements; graphical communicating shared resources; mobile robotic application; operational semantics; real-time systems; resource allocations; resource contentions; resource inherent constraints; resource requirements; safety analysis; safety properties; schedulability; scheduling disciplines; specification; temporal requirements; Algebra; Delay effects; Formal languages; Information analysis; Information science; Processor scheduling; Real time systems; Runtime; Safety; Telecommunication computing;
Conference_Titel :
Object-Oriented Real-Time Dependable Systems,1996. Proceedings of WORDS '96., Second Workshop on
Conference_Location :
Laguna Beach, CA
Print_ISBN :
0-8186-7570-5
DOI :
10.1109/WORDS.1996.506258