This paper develops a modeling paradigm called Architectural Interaction Diagrams, or AIDs, for the high-level design of systems containing concurrent, interacting components. The novelty of AIDs is that they introduce interaction mechanisms, or buses, as first-class entities into the modeling vocabulary. Users then have the capability, in their modeling, of using buses whose behavior captures interaction at a higher level of abstraction than that afforded by modeling notations such as Message Sequence Charts or process algebra, which typically provide only one fixed interaction mechanism. This paper defines AIDs formally by giving them an operational semantics that describes how buses combine subsystem transitions into system-level transitions. This semantics enables AIDs to be simulated; to incorporate subsystems given in different modeling notations into a single system model; and to use testing, debugging and model checking early in the system design cycle in order to catch design errors before they are implemented.
We argue that the evident utility of scenario-based modeling can be greatly enhanced when enriched with a mathematically precise notion of conditionality and partiality, such as that found in Triggered Message Sequence Charts (TMSCs). Unlike traditional Message Sequence Charts, the TMSC formalism allows scenarios to be conditional and partial, supports logical as well as behavioral operators for scenario composition, and is equipped with a refinement notion drawn from traditional process theory that provides a rigorous basis for stepwise development of specifications. This paper illustrates these points via the Center TRACON Automation System for flight control.
TRIM is a tool for analyzing system requirements expressed using Triggered Message Sequence Charts (TMSCs). TMSCs enhance MSCs with capabilities for expressing conditional and partial behavior and with a refinement ordering. This paper shows how the Concurrency Workbench of the New Century may be adapted to check refinements between TMSC specifications.
Triggered Message Sequence Charts (TMSCs) are a visual, mathematically precise notation for capturing system requirements as conditional and partial scenarios. This paper shows how TMSCs may be used to formalize two different requirements modeling methodologies. The first approach combines prescriptive (``do this'') and constraint-based (``don't do that'') requirements within a single specification; it is useful for composing localized subsystem requirements with global system ones. The second approach supports layered specifications in which partial descriptions of requirements may be elaborated on in a succession of steps; it is suitable for the incremental development of complex behavior in which ``error'' scenarios are ``layered on top of'' normative ones. Both methodologies derive their formal robustness from the notion of semantic refinement for TMSCs, which is based on DeNicola's and Hennessy's must preorder. Case studies are used to illustrate the utility of the work.
We present a process-algebraic language for Probabilistic I/O Automata (PIOA). To ensure that PIOA specifications given in our language satisfy the ``input-enabled'' property, which requires that all input actions be enabled in every state of a PIOA, we augment the language with a set of type inference rules. We also equip our language with a formal operational semantics defined by a set of transition rules. We present a number of results whose thrust is to establish that the typing and transition rules are sensible and interact properly. The central connection between types and transition systems is that if a term is well-typed, then in fact the associated transition system is input-enabled. We also consider two notions of equivalence for our language, weighted bisimulation equivalence and PIOA behavioral equivalence. We show that both equivalences are substitutive with respect to the operators of the language, and note that weighted bisimulation equivalence is a strict refinement of behavioral equivalence.
This paper reports on an effort to integrate two verification tools, the Concurrency Workbench of the New Century (CWB-NC) and PIOATool. Our aim is to build a single tool that combines the ``functional'' analysis capabilities of the CWB-NC with the compositional performance-analysis features of PIOATool. We discuss some of the issues involved in the integration, highlighting a particular integration paradigm in which one tool becomes a subshell of the other.
Rance Cleaveland Last modified: Thu Oct 26 15:43:32 Eastern Daylight Time 2006