Show simple item record

dc.contributor.authorHeddaya, Abdelsalamen_US
dc.contributor.authorFahmy, Amren_US
dc.date.accessioned2011-09-14T13:22:15Z
dc.date.available2011-09-14T13:22:15Z
dc.date.issued1994-12-05
dc.identifier.citationHeddaya, Abdelsalam; Fahmy, Amr. "OS Support for Portable Bulk Synchronous Parallel Programs”, Technical Report BUCS-1994-012, Computer Science Department, Boston University, December 5, 1994. [Available from: http://hdl.handle.net/2144/1482]
dc.identifier.urihttps://hdl.handle.net/2144/1482
dc.description.abstractPredictability -- 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, infinite 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.sponsorshipARPA (F19628-92-C-0113); NSF (CDA-9308833)en_US
dc.language.isoen_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-1994-012
dc.titleOS Support for Portable Bulk Synchronous Parallel Programsen_US
dc.typeTechnical Reporten_US


This item appears in the following Collection(s)

Show simple item record