No abstract available.

This paper describes a method for using property definition templates to support automatic analysis of source code for application-specific security properties. The method is illustrated on an example data flow property of a C program.

Recently, software practitioners, using model-based engineering and similar methods, have begun developing software from models. After creating a model of the required system behavior, a developer can obtain assurance of the model by validating that it captures the intended behavior and verifying that it satisfies critical properties. Invariants are important to both validation, as a check that the model's behavior matches the intended behavior, and verification, as auxiliaries in proving critical system properties, either automatically or with human guidance. A common approach to discovering invariants is to propose and then check candidate invariants. In contrast, our invariant generation techniques deduce invariants directly from the specification of a model. This paper presents more powerful versions of our earlier techniques for invariant generation and illustrates their utility for a real-world AirLock system.

A major problem in verifying the security of code is that the code's large size makes it much too costly to verify in its entirety. This article describes a novel and practical approach to verifying the security of code which substantially reduces the cost of verification. In this approach, the security property of interest is represented formally and a compact security model, containing only information needed to reason about the policy, is constructed. To reduce the cost of verification, the code to be verified is partitioned into three categories: Only the first category, less than 10% of the code, requires requires substantial effort to verify; the proof of the other two categories is relatively trivial. Our approach was developed to support a Common Criteria evaluation of the separation kernel of an embedded software system. This article describes 1) our techniques and theory for verifying the kernel code and 2) the artifacts produced: a Top Level Specification (TLS), a formal statement of the security property, a mechanized proof that the TLS satisfies the property, the partitioning of the code, and a demonstration that the code conforms to the TLS. The article also presents the formal argument that the kernel code conforms to the TLS and consequently satisfies the security property.

Based on our recent experience in four projects, each focused on either security-critical or safety-critical software, this paper evaluates several notions, widely held by RE researchers, for their utility in practical software development. It describes four notions which in our view work in practice and five others which do not.

Although many algorithms, hardware designs, and security protocols have been formally verified, formal verification of the security of software is still rare. This is due in large part to the large size of software, which results in huge costs for verification. This paper describes a novel and practical approach to formally establishing the security of code. The approach begins with a well-defined set of security properties and, based on the properties, constructs a compact security model containing only information needed to rea-son about the properties. Our approach was formulated to provide evidence for a Common Criteria evaluation of an embedded soft-ware system which uses a separation kernel to enforce data separation. The paper describes 1) our approach to verifying the kernel code and 2) the artifacts used in the evaluation: a Top Level Specification (TLS) of the kernel behavior, a formal definition of dataseparation, a mechanized proof that the TLS enforces data separation, code annotated with pre- and postconditions and partitioned into three categories, and a formal demonstration that each category of code enforces data separation. Also presented is the formal argument that the code satisfies the TLS.

A promising trend in software development is the increasing adoption of model-driven design. In this approach, a developer first constructs an abstract model of the required program behavior in a language, such as Statecharts or Stateflow, and then uses a code generator to automatically transform the model into an executable program. This approach has many advantages---typically, a model is not only more concise than code and hence more understandable, it is also more amenable to mechanized analysis. Moreover, automatic generation of code from a model usually produces code with fewer errors than hand-crafted code.One serious problem, however, is that a code generator may produce inefficient code. To address this problem, this paper describes a method for generating efficient code from SCR (Software Cost Reduction) specifications. While the SCR tabular notation and tools have been used successfully to specify, simulate, and verify numerous embedded systems, until now SCR has lacked an automated method for generating optimized code. This paper describes an efficient method for automatic code generation from SCR specifications, together with an implementation and an experimental evaluation. The method first synthesizes an execution-flow graph from the specification, then applies three optimizations to the graph, namely, input slicing, simplification, and output slicing, and then automatically generates code from the optimized graph. Experiments on seven benchmarks demonstrate that the method produces significant performance improvements in code generated from large specifications. Moreover, code generation is relatively fast, and the code produced is relatively compact.

This paper investigates the application of infinite state model checking to the formal analysis of requirements specifications in the SCR (software cost reduction) tabular notation using action language verifier (ALV). After reviewing the SCR method and tools and the action language, experimental results are presented of formally analyzing two SCR specifications using ALV, The application of ALV to verify or falsify (by generating counterexamples) the state and transition invariants of SCR specifications and to check disjointness and coverage properties is described. ALV is compared with the verification techniques that have been integrated into the SCR toolset

It is our great pleasure to welcome you to the Experience Reports Track of the 27th International Conference on Software Engineering (ICSE). The objective of the Experience Reports Track is to establish a dialogue between software practitioners and software engineering researchers on the benefits, obstacles, and weaknesses of applying software engineering principles, techniques, methods, processes, and tools in an industrial or organizational setting. In the call for papers, we invited four types of submissions: case studies, experience reports, experimental reports and problem statements. The call attracted 72 submissions from all over the world. The program committee of the Experience Reports Track accepted 14 submissions. The selection was based on at least three reviews per submission and the results of intensive consensus discussions prior to and during the Experience Reports Track program committee meeting, held on November 12, 2004 in Essen, Germany.The accepted papers of the ICSE 2005 Experience Reports Track cover topics such as agile methods, product lines, requirements engineering, software architecture, testing and verification. They document important lessons learned from applying software engineering principles, techniques, methods, processes, and tools in practice. Putting together the Experience Reports Track of ICSE 2005 was a team effort. We extend our sincerest gratitude to all of the people who helped us shape this event, especially to the members of our program committee and the ICSE 2005 organizing committee and to Richard van de Stadt, Andreas Metzger, and Nelufar Ulfat-Bunyadi. We hope that you find the Experience Reports Track of ICSE 2005 interesting and thought-provoking.

Although research in automated verication has produced very promising results, the question of how to effectively integrate these results into the software and hardware development processes is still unresolved. Typically, fully automated verication techniques are not scalable, and scalable verication techniques require substantial user guidance. Alternatively, developers could facilitate scalable verication by constructing software and hardware systems in ways that make them easier to verify. In this panel we will discuss the idea of design for verication.

This industrial panel is organized to discuss the views, experiences and opinions of formal methods practitioners frclni desigri automation, hardware and sofhyare industries, in order to understand rlie industrial needs ar7d trends in rising fnmial methods. In particulas we discuss the currertt tlinist or1 application of fnmlal verificntion in software duveekopnient, and what liurdware fomiai verification experiences bring to bear forfim” sofhvare verification.

A critical issue in software engineering is how to construct high assurance software systems, i.e., software Systems where compelling evidence is required that the system delivers its services in a manner satisfying critical properties, such as safety and security. This two-day XSE workshop, the third in a series of workshops on high assurance systems, will provide a forum for researchers and practitioners to exchange ideas and experiences relevant to the development of software for aerospace systems, medical systems, systems controlling nuclear power plants, and other critical systems. Participants of the SEHAS 2003 workshop will explore the opportunities for, and benefits of, synergies between three important themes-product, process, and profiling-each theme reflecting an important aspect of software development for high assurance systems.

This paper describes a compositional proof strategy for verifying properties of requirements specifications. The proof strategy, which may be applied using either a model checker or a theorem prover, uses known state invariants to prove state and transition invariants. Two proof rules are presented: a standard incremental proof rule analogous to Manna and Pnueli's incremental proof rule and a compositional proof rule. The advantage of applying the compositional rule is that it decomposes a large verification problem into smaller problems which often can be solved more efficiently than the larger problem. The steps needed to implement the compositional rule are described, and the results of applying the proof strategy to two examples, a simple cruise control system and a real-world Navy system, are presented. In the Navy example, compositional verification %based on the compositional proof using either theorem proving or model checking was three times faster than verification %model checking using based on the standard incremental (noncompositional) rule. In addition to the two above rules for proving invariants, a new compositional proof rule is presented for circular assume-guarantee proofs of invariants. While in principle the strategy and %the rules described for proving invariants may be applied to any state-based specification with parallel composition of components, the specifications in the paper are expressed in the SCR (Software Cost Reduction) tabular notation, the auxiliary invariants used in the proofs are automatically generated invariants, and the verification is supported by the SCR tools.

We favor an approach to building secure systems that includes an application-based security model. An instance of such a model and its formalization have been presented. Important aspects of the model are: (1) because it is framed in terms of operations and data objects that the user sees, the model captures the system's security requirements in a way that is understandable to users; (2) the model defines a hierarchy of entities and references; access to an entity can be controlled based on the path used to refer to it; (3) because the model avoids specifying implementation strategies, software developers are free to choose the most effective implementation; (4) the model and its formalization provide a basis for certifiers to assess the security of the system as a whole. Simplicity and clarity in the model's statement have been primary goals. The model's statement does not, however, disguise the complexity that is inherent in the application. In this respect, we have striven for a model that is as simple as possible but stops short of distorting the user's view of the system. The work reported demonstrates the feasibility of defining an application-based security model informally and subsequently formalizing it.

In earlier work (Jeffords and Heitmeyer, 1998) we developed a fixpoint algorithm for automatically generating state invariants, properties that hold in each reachable state of a state machine model, from state-based requirements specifications. Such invariants are useful both in validating requirements specifications and as auxiliary lemmas in proofs that a requirements specification satisfies other invariant properties. This paper describes a new related algorithm that strengthens state invariants generated by our initial algorithm and demonstrates the new algorithm on a simplified version of an automobile cruise control system. The paper concludes by describing how the two algorithms were used to generate state invariants from a requirements specification of a cryptographic device and how the invariants in conjunction with a theorem prover were used to prove formally that the device satisfies a set of critical security properties.

This paper describes MTSim, an extensible, customizable simulation platform for the Modechart toolset (MT). MTSim provides support for "plugging in" user-defined viewers useful in simulating system behavior in different ways, including application-specific ways. MTSim also supports full user participation in the generation of simulations by allowing users to inject events into the execution trace. Moreover, MTSim provides monitoring and assertion checking of execution traces and the invocation of user-specified handlers upon assertion violation. This paper also introduces an MTSim component called WebSim, a suite of simulation tools for MT, and an application-specific component of MTSim which displays the cockpit of an F-18 aircraft and which responds to user inputs to model a bomb release function.

To date, the tabular based SCR (Software Cost Reduction) method has been applied mostly to the development of embedded control systems. The paper describes the successful application of the SCR method, including the SCR* toolset, to a different class of system, a COMSEC (Communications Security) device called CD that must correctly manage encrypted communications. The paper summarizes how the tools in SCR* were used to validate and to debug the SCR specification and to demonstrate that the specification satisfies a set of critical security properties. The development of the CD specification involved many tools in SCR*: a specification editor, a consistency checker, a simulator, the TAME interface to the theorem prover PVS, and various other analysis tools. Our experience provides evidence that use of the SCR* toolset to develop high quality requirements specifications of moderately complex COMSEC systems is both practical and low cost.

Automatic generation of state invariants, properties that hold in every reachable state of a state machine model, can be valuable in software development. Not only can such invariants be presented to system users for validation, in addition, they can be used as auxiliary assertions in proving other invariants. This paper describes an algorithm for the automatic generation of state invariants that, in contrast to most other such algorithms, which operate on programs, derives invariants from requirements specifications. Generating invariants from requirements specifications rather than programs has two advantages: 1) because requirements specifications, unlike programs, are at a high level of abstraction, generation of and analysis using such invariants is easier, and 2) using invariants to detect errors during the requirements phase is considerably more cost-effective than using invariants later in software development. To illustrate the algorithm, we use it to generate state invariants from requirements specifications of an automobile cruise control system and a simple control system for a nuclear plant. The invariants are derived from specifications expressed in the SCR (Software Cost Reduction) tabular notation.

Exposing inconsistencies can uncover many defects in software specifications. One approach to exposing inconsistencies analyzes two redundant specifications, one operational and the other property-based, and reports discrepancies. This paper describes a "practical" formal method, based on this approach and the SCR (software cost reduction) tabular notation, that can expose inconsistencies in software requirements specifications. Because users of the method do not need advanced mathematical training or theorem-proving skills, most software developers should be able to apply the method without extraordinary effort. This paper also describes an application of the method which exposed a safety violation in the contractor-produced software requirements specification of a sizable, safety-critical control system. Because the enormous state space of specifications of practical software usually renders direct analysis impractical, a common approach is to apply abstraction to the specification. To reduce the state space of the control system specification, two "pushbutton" abstraction methods were applied, one which automatically removes irrelevant variables and a second which replaces the large, possibly infinite, type sets of certain variables with smaller type sets. Analyzing the reduced specification with the model checker Spin uncovered a possible safety violation. Simulation demonstrated that the safety violation was not spurious but an actual defect in the original specification.

No abstract available.

This article describes a formal analysis technique, called consistency checking , for automatic detection of errors, such as type errors, nondeterminism, missing cases, and circular definitions, in requirements specifications. The technique is designed to analyze requirements specifications expressed in the SCR (Software Cost Reduction) tabular notation. As background, the SCR approach to specifying requirements is reviewed. To provide a formal semantics for the SCR notation and a foundation for consistency checking, a formal requirements model is introduced; the model represents a software system as a finite-state automation which produces externally visible outputs in response to changes in monitored environmental quantities. Results of two experiments are presented which evaluated the utility and scalability of our technique for consistency checking in real-world avionics application. The role of consistency checking during the requirements phase of software development is discussed.

Summary form only given, as follows. Static models are not appropriate for next-generation distributed real-time applications that are likely to be adaptive in nature, (for example, to provide a high degree of fault tolerance). During the last few years, the real-time systems community has started to counter this criticism by extending traditional work to cover newer application domains, The central problem remains, however, that the concept of adaptivity is often domain-specific and sometimes ill-defined in the context of bringing distributed real-time systems concept into better focus. Accordingly, be it resolved that future distributed embedded and real-time applications will be adaptive and that meanings, challenges and research paradigms await discovery. The charge to the panel is to defend (or to dismiss as fluff) the above resolution.

The paper describes a class of formal analysis called consistency checking that mechanically checks requirements specifications, expressed in the SCR tabular notation, for application independent properties. Properties include domain coverage, type correctness, and determinism. As background, the SCR notation for specifying requirements is reviewed. A formal requirements model describing the meaning of the SCR notation is summarized, and consistency checks derived from the formal model are described. The results of experiments to evaluate the utility of automated consistency checking are presented. Where consistency checking of requirements fits in the software development process is discussed.

A new solution to the generalized railroad crossing problem, based on timed automata, invariants and simulation mappings, is presented and evaluated. The solution shows formally the correspondence between four system descriptions: an axiomatic specification, an operational specification, a discrete system implementation, and a system implementation that works with a continuous gate model.>

This paper introduces MT, a collection of integrated tools for specifying and analyzing real-time systems using the Modechart language. The toolset includes facilities for creating and editing Modechart specifications. Users may symbolically execute the specifications with an automatic simulation tool to make sure that the specified behavior is what was intended. They may also invoke a verifier that uses model-checking to determine whether the specifications imply (satisfy) any of a broad class of safety assertions. To illustrate the toolset's capabilities as well as several issues that arise when formal methods are applied to real-world systems, the paper includes specifications and analysis procedures for a software component taken from an actual Naval real-time system.>

Increasing use of automation in computer systems, such as advanced cockpits, presents special challenges in the design of user interfaces. The challenge is particularly difficult when automation is intermittent because the interface must support smooth transitions from automated to manual mode. A theory of direct manipulation predicts that this interface style will smooth the transition. Interfaces were designed to test the prediction and to evaluate two aspects of direct manipulation, semantic distance and engagement. Empirical results supported the theoretical prediction and also showed that direct engagement can have some adverse effects on another concurrent manual task. Generalizations of our results to other complex systems are presented.

To provide a firm foundation for proofs about the security properties of a system specification or implementation, a formal statement of its security model is needed. This paper presents a formal model that corresponds to an informal, application-based security model for military message systems (MMS) that has been documented elsewhere. Following the formal statement, some considerations that led to its present form are discussed. The paper concludes with the statement of a "Basic Security Theorem" for the model.

Military systems that process classified information must operate in a secure manner; that is, they must adequately protect information against unauthorized disclosure, modification, and withholding.A goal of current research in computer security is to facilitate the construction of multilevel secure systems, systems that protect information of different classifications from users with different clearances.Security models are used to define the concept of security embodied by a computer system.A single model, called the Bell and LaPadula model, has dominated recent efforts to build secure systems but has deficiencies.We are developing a new approach to defining security models based on the idea that a security model should be derived from a specific application.To evaluate our approach, we have formulated a security model for a family of military message systems.This paper introduces the message system application, describes the problems of using the Bell-LaPadula model in real applications, and presents our security model both informally and formally.Significant aspects of the security model are its definition of multilevel objects and its inclusion of application-dependent security assertions.Prototypes based on this model are being developed.

An abstract requirements specification states system requirements precisely without describing a real or a paradigm implementation. Although such specifications have important advantages, they are difficult to produce for complex systems and hence are seldom seen in the "real" programming world. This paper introduces an approach to producing abstract requirements specifications that applies to a significant class of real-world systems, including any system that must reconstruct data that have undergone a sequence of transformations. tions. It also describes how the approach was used to produce a requirements document for SCP, a small, but nontrivial Navy communications system. The specification techniques used in the SCP requirements document are introduced and illustrated with examples.

The need for timely message delivery coupled with decreasing computer costs is causing message handling in the Department of Defense to be increasingly automated. This paper describes the functional, security, and performance requirements of automated military message systems. In light of these requirements, four operational message systems are compared and contrasted. A summary of results is presented for the Military Message Experiment, a study of the military utility of automated message systems. The usefulness of advanced software engineering technology, especially the family methodology, is explored for military message automation. Finally, several trends and research issues in military message handling are identified.