Loading...
Please wait, while we are loading the content...
Similar Documents
Gcsr: a Graphical Language for the Speciication and Reenement of Real-time Systems
| Content Provider | Semantic Scholar |
|---|---|
| Author | Ben-Abdallah, Hanêne |
| Copyright Year | 1995 |
| Abstract | The potential high cost associated with the malfunctioning of real-time systems created a need for a formal framework where a real-time system can be precisely speci ed and rigorously analyzed before its implementation. Although various formal methods for realtime systems have been developed, they tend to be inaccessible to practitioners because of their mathematical textual notations that often produce obtuse speci cations. We propose Graphical Communicating Shared Resources, GCSR, a formal language for the speci cation, analysis and re nement of real-time systems including their functional and resource requirements. GCSR allows a modular and hierarchical, thus, scalable description of a real-time system. It supports notions of communication through events, interrupt, concurrency, and time to describe the functional requirements of a real-time system. In addition, GCSR allows the explicit representation of resources and priorities to resolve resource contention in such a way that produces easy to understand and modify speci cations. The semantics of GCSR is the Algebra of Communicating Shared Resources, a timed process algebra with operational, i.e., executable semantics. The equivalence notions of ACSR make it possible to verify that GCSR speci cations, e.g., design and requirements behave the same. To support the top-down, modular development of a real-time speci cation in GCSR, we propose a re nement theory for ACSR and thus GCSR. ACSR re nement consists of relabeling and action re nement. Communication events in an ACSR speci cation can be re ned by relabelling them. Time and resource-consuming actions in ACSR can be re ned by syntactically replacing themwith processes that may have communication events and use less resources than the re ned actions. We de ne consistency between an abstract speci cation and a re ned speci cation in terms of ordering relations over traces. The trace ordering relations relate traces that share timing properties such as equal duration and preservation of timed occurrences of communication events of the abstract speci cation. To facilitate our notion of re nement, we develop a set of transformation rules that syntactically rewrite a speci cation to a re ned one. The transformation rules will help de ne GCSR re nements. |
| File Format | PDF HTM / HTML |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
