This paper shows how an architecture description notation that has support for timed events can be used to provide a meta-language for specifying exact communication semantics. The advantages of such an approach is that a designer is made fully aware of the ramifications of her design choices so that an attacker can no longer take advantage of hidden assumptions.
This paper describes a framework for modeling and validating distributed real-time embedded control systems. The modeling component of the framework combines executable architectural specifications with component models in notations such as Simulink® and Stateflow® to yield simulate-able models of distributed systems. The paper then discusses techniques for comparing the behavior of these system models with idealized control specifications given as single Simulink / Stateflow models. The framework is intended to support design processes in which a controls engineer develops a controller model that is then used as a specification by a system-engineering team responsible for a system model involving deployment-platform details. The V&V strategies proposed are derived from research into software V&V developed in the Computer Science community. The approaches outlined in the paper are intended to enable engineers to develop distributed embedded controller networks more quickly, and with much greater confidence in their correctness.
This paper introduces Triggered Message Sequence Charts (TMSCs), a graphical, mathematically well-founded framework for capturing scenario-based system requirements of distributed systems. Like Message Sequence Charts (MSCs), TMSCs are graphical depictions of scenarios, or exchanges of messages between processes in a distributed system. Unlike MSCs, however, TMSCs are equipped with a notion of trigger that permits requirements to be made conditional; a notion of partiality indicating that a scenario may be subsequently extended; and a notion of refinement for assessing whether or not a more detailed specification correctly elaborates on a less detailed one. The TMSC notation also includes a collection of composition operators allowing structure to be introduced into scenario specifications, so that interactions among different scenarios may be studied. In the first part of this paper, TMSCs are introduced, and their use in support of requirements modeling is illustrated via two extended examples. The second part develops the mathematical underpinnings of the language.
Working in the context of a process-algebraic language for Probabilistic I/O Automata (PIOA), we study the notion of PIOA behavior equivalence by obtaining a complete axiomatization of its equational theory and comparing the results with a complete axiomatization of a more standard equivalence, weighted bisimulation. The axiomatization of behavior equivalence is achieved by adding to the language an operator for forming convex combinations of terms.
Rance Cleaveland Last modified: Thu Oct 26 16:13:19 Eastern Daylight Time 2006