This paper discusses the results of an application of a formally based verification technique, called Instrumentation-Based Verification (IBV), to a production automotive lighting controller. The goal of the study is to assess, from both a tools as well as a methodological perspective, the performance of IBV in an industrial setting. The insights obtained as a result of the project include a refinement of a previously developed architecture for requirements specifications; observations about changes to model-based design workflows; insights into the role of requirements during development; and the capability of automated verification to detect inconsistencies among requirements as well as between requirements and design models.

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 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.

With security becoming an important concern for both users as well as designers of large-scale software systems, it is necessary to introduce security considerations very early in the system development life-cycle namely in the modeling phase itself. But the main problem in the widespread adoption of security modeling has been that representations of even moderate-size systems consume so much memory (due to the infamous state space explosion problem) that designers are loathe to spend time increasing the complexity of their models by introducing security aspects in the design phase itself. In this paper we propose a technique called security check which entails taking small units of a system, putting them in a "security harness" that exercises relevant executions appropriately within the unit, and then model checking these more tractable units. For most systems whose security requirements are localized to individual system components or interactions between small numbers of components, security check offers a means of coping with state explosion. Another major benefit of security check is that it enables us to detect system vulnerabilities even when the attack behavior is not known. And for known attack patterns security check can provide models of suspicious behavior which can then be used for intrusion detection at a later stage.