OpenBU

Building Responsive Systems from Physically-correct Specifications

OpenBU

Show simple item record

dc.date.accessioned 2011-09-12T13:33:39Z
dc.date.available 2011-09-12T13:33:39Z
dc.date.issued 1993-10
dc.identifier.uri http://hdl.handle.net/2144/1466
dc.description.abstract Predictability - the ability to foretell that an implementation will not violate a set of specified reliability and timeliness requirements - is a crucial, highly desirable property of responsive embedded systems. This paper overviews a development methodology for responsive systems, which enhances predictability by eliminating potential hazards resulting from physically-unsound specifications. The backbone of our methodology is the Time-constrained Reactive Automaton (TRA) formalism, which adopts a fundamental notion of space and time that restricts expressiveness in a way that allows the specification of only reactive, spontaneous, and causal computation. Using the TRA model, unrealistic systems - possessing properties such as clairvoyance, caprice, in finite capacity, or perfect timing - cannot even be specified. We argue that this "ounce of prevention" at the specification level is likely to spare a lot of time and energy in the development cycle of responsive systems - not to mention the elimination of potential hazards that would have gone, otherwise, unnoticed. The TRA model is presented to system developers through the CLEOPATRA programming language. CLEOPATRA features a C-like imperative syntax for the description of computation, which makes it easier to incorporate in applications already using C. It is event-driven, and thus appropriate for embedded process control applications. It is object-oriented and compositional, thus advocating modularity and reusability. CLEOPATRA is semantically sound; its objects can be transformed, mechanically and unambiguously, into formal TRA automata for verification purposes, which can be pursued using model-checking or theorem proving techniques. Since 1989, an ancestor of CLEOPATRA has been in use as a specification and simulation language for embedded time-critical robotic processes. en_US
dc.description.sponsorship Harvard University; DARPA (N00039-88-C-0163) en_US
dc.language.iso en_US en_US
dc.publisher Boston University Computer Science Department en_US
dc.relation.ispartofseries BUCS Technical Reports;BUCS-TR-1993-012
dc.title Building Responsive Systems from Physically-correct Specifications en_US
dc.type Technical Report en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search OpenBU


Browse

Deposit Materials

Statistics