Abstract Safety critical systems, such as medical, automotive, and avionics systems, play an important role in our daily lives. Increasing demand for new technologies in these safety critical systems requires rapid adoption of commercial hardware and software. However, the adoption of new hardware and software increases life‐threatening vulnerabilities. To aid in the reduction of these vulnerabilities and system failures, this paper proposes a framework based on formal methods for developing safety‐critical systems from requirements analysis to code generation. This framework includes a development process for documenting system requirements using tabular expressions, automatic formal model generation from the documented requirements, verification and validation of the generated formal models using proof techniques and animations, interactive simulation for validating the required behavior of the developed models by enabling domain experts to observe the system states according to, and finally, code generation from the formal model into a desired language. A prototype toolchain is developed to automate this framework. An assessment of the proposed framework is undertaken through a case study: insulin infusion pump (IIP).

The theory of institutions, introduced by Goguen and Burstall in 1984, can be thought of as an abstract formulation of model theory. This theory has been shown to be particularly useful in computer science, as a mathematical foundation for formal approaches to software construction. Institution theory was extended by a number of researchers, José Meseguer among them, who, in 1989, presented General Logics, wherein the model theoretical view of institutions is complemented by providing (categorical) structures supporting the proof theory of any given logic. In other words, Meseguer introduced the notion of proof calculus as a formalisation of syntactical deduction, thus “implementing” the entailment relation of a given logic. In this paper we follow the approach initiated by Goguen and introduce the concept of Satisfiability Calculus. This concept can be regarded as the semantical counterpart of Meseguer’s notion of proof calculus, as it provides the formal foundations for those proof systems that resort to model construction techniques to prove or disprove a given formula, thus “implementing” the satisfiability relation of an institution. These kinds of semantic proof methods have gained a great amount of interest in computer science over the years, as they provide the basic means for many automated theorem proving techniques.

Assurance is a demonstration that a complex system (such as a car or a communication network) possesses an importantproperty, such as safety or security, with a high level of confidence. In contrast to currently dominant approaches to building assurance cases, which are focused on goal structuring and/or logical inference, we propose considering assurance as a model transformation (MT) enterprise: saying that a system possesses an assured property amounts to saying that a particular assurance view of the system comprising the assurance data, satisfies acceptance criteria posed as assurance constraints. While the MT realizing this view is very complex, we show that it can be decomposed into elementary MTs via a hierarchy of refinement steps. The transformations at the bottom level are ordinary MTs that can be executed for data specifying the system, thus providing the assurance data to be checked against the assurance constraints. In this way, assurance amounts to traversing the hierarchy from the top to the bottom and assuring the correctness of each MT in the path. Our approach has a precise mathematical foundation (rooted in process algebra and category theory) --- a necessity if we are to model precisely and then analyze our assurance cases. We discuss the practical applicability of the approach, and argue that it has several advantages over existing approaches.

Abstract We present a formal characterization of fault-tolerant behaviors of computing systems via simulation relations. This formalization makes use of variations of standard simulation relations in order to compare the executions of a system that exhibits faults with executions where no faults occur; intuitively, the latter can be understood as a specification of the system and the former as a fault-tolerant implementation. By employing variations of standard simulation algorithms, our characterization enables us to algorithmically check fault-tolerance in polynomial time, i.e., to verify that a system behaves in an acceptable way even subject to the occurrence of faults. Furthermore, the use of simulation relations in this setting allows us to distinguish between the different levels of fault-tolerance exhibited by systems during their execution. We prove that each kind of simulation relation preserves a corresponding class of temporal properties expressed in CTL; more precisely, masking fault-tolerance preserves liveness and safety properties, nonmasking fault-tolerance preserves liveness properties, while failsafe fault-tolerance guarantees the preservation of safety properties. We illustrate the suitability of this formal framework through its application to standard examples of fault-tolerance.

Software has come to mediate many of the activities in life, including financial service platforms, social networks and vehicle control. As a result, governing bodies have responded to this trend by creating standards and regulations to address issues such as safety and privacy. In this context, the compliance of software development to standards and regulations has emerged as a key issue. For software development organizations, compliance is a complex and costly goal to achieve. They may have to comply with multiple standards due to multiple jurisdictions or to address different aspects of the software and these may overlap and conflict with each other. The evolution of standards must be tracked and changes assessed. Evidence for claims of compliance must be collected and managed. Finally, maintaining families of related software products (product lines) further multiplies the effort. In this paper, we propose to exploit the connection between the field of model management and the problem of compliance management and explore how to use model management techniques to address software compliance management issues.

Feature modeling is the most common approach to specify software product lines. The main part of a feature model is a special tree of features called a feature diagram. Cardinality-based feature diagrams provide the most expressive tool among the current feature diagram languages. The most common characterization of the semantics of a cardinality-based diagram is the set of flat multisets over features satisfying the constraints. However, this semantics provides a poor abstract view of the diagram. We address this problem by proposing another multiset theory for the diagram, called the hierarchical theory. We show that the theory captures all information of the diagram so that one can retrieve the diagram from its theory. This provides us with a theoretical framework for addressing some challenging issues in feature modeling, e.g., feature model management and reverse engineering of feature models.

Abstract In this paper we present a formalization of the Z notation and its structuring mechanisms. One of the main features of our formal framework, based on category theory and the theory of institutions, is that it enables us to provide an abstract view of Z and its related concepts. We show that the main structuring mechanisms of Z are captured smoothly by categorical constructions. In particular, we provide a straightforward and clear semantics for promotion, a powerful structuring technique that is often not presented as part of the schema calculus. Here we show that promotion is already an operation over schemas (and more generally over specifications), that allows one to promote schemas that operate on a local notion of state to operate on a subsuming global state, and in particular can be used to conveniently define large specifications from collections of simpler ones. Moreover, our proposed formalization facilitates the combination of Z with other notations in order to produce heterogeneous specifications, i.e., specifications that are obtained by using various different mathematical formalisms. Thus, our abstract and precise formulation of Z is useful for relating this notation with other formal languages used by the formal methods community. We illustrate this by means of a known combination of formal languages, namely the combination of Z with CSP .

We present a novel and general technique for automated test generation that combines tight bounds with incremental SAT solving. The proposed technique uses incremental SAT to build test suites targeting a specific testing criterion, amongst various black-box and white-box criteria. As our experimental results show, the combination of tight bounds with incremental SAT, and the testing criterion driven approach implemented in our prototype tool FAJITA, enable us to effectively generate test suites for container classes with rich contracts, more efficiently than other state-of-the-art tools.

Architecture Description Languages (ADLs) were developed to support the abstract level of software structuring that is the subject matter of software architecture. Community is an ADL built on co-ordination principles and a categorical framework to support the composition of specifications of components to form the system's specification. However, an important shortcoming of Community is the lack of integrated support for specifying the system's architectural changes in both the set of components and the connections between them. This paper presents DynaComm, an extension of Community to support hierarchical design and dynamic reconfiguration of component based systems. The architectural design principles supported by the DynaComm language are illustrated through the design of a fault-tolerant, dynamic client-server system. A state anchored semantics of DynaComm is given by reducing a DynaComm design to a Community design, i.e., a configuration of components, cables and superposition morphisms, and then taking the colimit of the Community diagram. The careful use of extension, refinement and superposition morphisms guarantees that this is always possible.

The computer controlled shutdown systems for the Nuclear Power Generating Station at Darlington, Canada, have been subject to licensing scrutinization on a number of occasions. After the first licence was approved in 1990, the licensee, Ontario Hydro, was given a number of years by the regulator to redesign the shutdown systems so that they would be more maintainable. This paper briefly describes the original certification process, lessons learned, and the subsequent development and certification of the shutdown systems. The development, internal certification processes and the regulator's certification process are briefly described. Although twenty years has elapsed since this work started, and there are new analysis techniques and tools that could be applied today, the original process itself has withstood the test of time extraordinarily well. This paper describes principles that explain why it was so successful, and how we can develop more modern approaches from this experience.

In the present paper we use a variation of a well-known example (dining philosophers) to illustrate how deontic logics can be used to specify, and verify, systems with fault- tolerant characteristics. Towards this goal, we first introduce our own version of a prepositional deontic logic, and then some of its most important meta properties are described. Our main goal is to show that our deontic formalism is suitable for use in practical examples, and also to prepare the ground for more inclusive formalisms.

This paper proposes the development of a logic for verifying properties of programs in rewriting logic. Rewriting logic is primarily a logic of change, in which deduction corresponds directly to computation, and not a logic to talk about change in a more indirect and global manner, such as the different modal and temporal logics that can be found in the literature. We start by defining a modal action logic (VLRL) in which rewrite rules are captured as actions. The main novelty of this logic is a topological modality associated with state constructors that allows us to reason about the structure of states, stating that the current state can be decomposed into regions satisfying certain properties. Then, on top of the modal logic, we define a temporal logic for reasoning about properties of the computations generated from rewrite theories, and demonstrate its potential by means of several examples.

We study a number of restrictions associated with the first-order relational specification language Alloy. The main shortcomings we address are:---the lack of a complete calculus for deduction in Alloy's underlying formalism, the so called relational logic,---the inappropriateness of the Alloy language for describing (and analyzing) properties regarding execution traces.The first of these points was not regarded as an important issue during the genesis of Alloy, and therefore has not been taken into account in the design of the relational logic. The second point is a consequence of the static nature of Alloy specifications, and has been partly solved by the developers of Alloy; however, their proposed solution requires a complicated and unstructured characterization of executions.We propose to overcome the first problem by translating relational logic to the equational calculus of fork algebras . Fork algebras provide a purely relational formalism close to Alloy, which possesses a complete equational deductive calculus. Regarding the second problem, we propose to extend Alloy by adding actions . These actions, unlike Alloy functions, do modify the state. Much the same as programs in dynamic logic, actions can be sequentially composed and iterated, allowing them to state properties of execution traces at an appropriate level of abstraction.Since automatic analysis is one of Alloy's main features, and this article aims to provide a deductive calculus for Alloy, we show that:---the extension hereby proposed does not sacrifice the possibility of using SAT solving techniques for automated analysis,---the complete calculus for the relational logic is straightforwardly extended to a complete calculus for the extension of Alloy.

During the last two decades, a lot of effort has been focused on automating the generation of software applications. The automation process can start early, after some manual stage(s) or following (a) previous automatic stage(s). Such automation tools should have the capability of generating executable programs, specifications, or formal requirements, as appropriate. The requirements gathering and checking is considered as the most important phase to eliminate bugs that appear later and may be removed during the design or implementation phases, but with higher cost and effort. The GOPCSD (goal-oriented process control systems design) tool is designed to gather and structure the requirements for process control systems. The tool achieves separation between the process system engineer's view and the software engineer's. The tool hides the mathematic details of B method from the system engineer; enabling him to focus only on the operation specifications while the software engineer within the B toolkit environment focuses on programming paradigms. Some adaptations have been applied to the method of KAOS in order to yield maximum benefit while minimizing both the required time and the effort to complete the gathering of application requirements for process control systems. After studying different process control case studies, six patterns have been identified: two (alternative and conjunction pattern) of them extending the existing patterns in the KAOS method and four (sequence, disjunction, simultaneous, and inheritance patterns) are new and can be extensively found within the process control systems.

We propose a formal specification language for dynamically reconfigurable component-based systems, based on temporal logic. The main aim of the language is to allow one to specify behaviours of component-based systems declaratively, with special emphasis on behaviours in which the architectural structure of the system changes dynamically. Due to the semantics and organisation of our language, it is straightforward to hierarchically build reconfigurable systems in terms of subsystems and basic component parts, and reason about them within the language. Despite its expressive power, the language is rather simple.

Discussions of the role of mathematics in software engineering are common and have probably not changed much over the last few decades. There is now much discussion about the "intuitive" nature of software construction and analogies are drawn (falsely) with graphic design, (conventional) architecture, etc. The conclusion is that mathematics is an unnecessary luxury and that, like these other disciplines, it is not needed in everyday practice. We attempt to refute these arguments by recourse to ideas from the philosophy of science developed over the past century. We demonstrate why these ideas are applicable, why they establish a framework (in the sense of Carnap) in which many central ideas in software engineering can be formalised and organised, why they refute the simplistic recourse to "intuition", and why they provide a scientific/engineering framework in which contributions to the theory and practice of software engineering can be judged.

For the last three years the authors have been building an instantiation of a system development paradigm, called ARTS. The paradigm consists of a view of what a system development environment is, in general terms, and a methodology for instantiating the paradigm for particular and specific domains of application. The motivation for and the explanation of the paradigm are derived from extant epistemological models of the method of natural science. They assert that these models are directly applicable to the domain of software and systems construction, and that, from them, one can derive principles and explanations for what a software development environment should be. They present briefly the statement view of scientific theories, a conceptual architecture for software development environments whose rationale is given in terms of the statement view and some examples of how the present version of ARTS realises this conceptual architecture.

The connection between some modularity properties and interpolation is revisited and restated in a general "logic-independent" framework. The presence of uniform interpolants is shown to assist in certain proof obligations, which suffice to establish the composition of refinements. The absence of the desirable interpolation properties from many logics that have been used in refinement motivates a thorough investigation of methods to expand a specification formalism orthogonally, so that the critical uniform interpolants become available. A potential breakthrough is outlined in this paper.

The necessity to deal simultaneously with different formalisms seems to be intrinsic to the discipline of Software Engineering, particularly in relation to modularity, reusability and incremental ity. In order to accommodate this diversity of formalisms, some authors have proposed the adoption of a common semantic domain for the different specification languages, and their transla tion into a common style of predicate logic. In this paper, we suggest that an alternative approach may be taken where the different modelling approaches are formalised individually in a common mathematical framework – Category Theory, and relationships are established between them using functors. Several examples are adduced to support this view and the generality of the approach is illustrated by formalising reusability as a property of a functor relating two such formalisms.

Recent research has advocated the use of deontic logics in requirements specification. A form of deontic action logic is described, and it is shown how it can be used to specify both temporal constraints and error recovery. The logic includes a deontic predicate of bounded obligation, and normative predicates. Bounded obligation allows bounds to be placed on the performance of actions, and can be used to specify temporal constraints. The formalism also allows the removal and extension of obligations before they must be met. The normative predicates indicate when a system has performed an action normally or abnormally, and allow the specification of corrective actions that recover from error situations.>

Abstract In this paper, we bring together the use of temporal logic for specifying concurrent systems, in the tradition initiated by A. Pnueli, and the use of tools from category theory as a means for structuring specifications as combinations of theories in the style developed by R. Burstall and J. Goguen. As a result, we obtain a framework in which systems of interconnected components can be described by assembling the specifications of their components around a diagram, using theory morphisms to specify how the components interact. This view of temporal theories as specification units naturally brings modularity to the description and analysis of systems. Moreover, it becomes possible to import into the area of formal development of reactive systems the wide body of specification techniques that have been defined for structuring specifications independently of the underlying logic, and that have been applied with great success in the area of Abstract Data Types. Finally, as a discipline of design, we use the object-oriented paradigm according to which components keep private data and interact by sharing actions, with a view towards providing formal tools for the specification of concurrent objects.

This work provides a constructive presentation of modal logis in natural deduction style. The modal connective □ is presented in a constructive form, which can be considered as an operational semantics for it. Modal connectives have been recognized as intentional connectives for a long time, but modal logicians have insisted in using extensional techniques to deal with them. In this paper, the modal connective is presented as a higher-order connective defined on top of the object level logical connectives. The simplest version of our system of modal logic with classical negation coincides with the classical modal logic K. The most important modal logics have an elegant presentation in this system. T, S4, S5, D, D4, D5 are presented, without any side effect condition on the structure of the deductions. Most presentations of intuitionistic modal logics fail in giving an intuitionistic interpretation to the modal connective. In general, such interpretations are based on some alien element (for instance, the accessibility relation), which are by no means intuitionistic. In the system described here it is not only possible to present an intuitionistic interpretation of the modal connective □, which takes into account only deducibility issues, but also to give a constructive natural deduction presentation for the □.

Starting from a deontic specification modelling the behaviour of a system, we show how it is possible to reason about the temporal properties of the normative behaviours of that system. In particular, we show how safety and liveness properties can be derived, respectively, from permission and obligation structures. A formal relationship is thus established between the recently proposed deontic accounts of behaviour, that are more action-oriented, and the already traditional and successful property-oriented frameworks based on temporal logics.

Formal techniques exist for the crucial specification phase in the design of systems, including database applications. We briefly indicate the potential benefits of the so-called abstract data type discipline and show how it might be made more palatable to the non-mathematician. This is done through the mechanism of traces. This tool is used both as a mechanism for modelling (in an executable manner) the application and as a basis for a methodology which can be used in the development of a formal algebraic specification.

We present in this report a method of database specification which overcomes a severe drawback of most database models and specification techniques – namely the inability to formalise the concept of database instance (state). The lack of formalisation of this concept in a model results in the inability to present a uniform treatment of queries and updates. We indicate why previous models and specification techniques are inadequate in this respect and then develop a modelling technique to overcome this situation. The use of algebraic specification tools in conjunction with this technique is illustrated in the specification of an example database.

Data types can be elegantly characterized as the algebraic quotient of the initial algebra in the appropriate class of algebras. In this paper, data types whose domain is continuous (continuous data types) are defined and studied. It is shown that an algebraic quotient of the appropriate initial continuous algebra can be used to characterize continuous data types when certain conditions are satisfied. Two well-known computer science examples are presented to illustrate the results. These types are lists, including infinite lists and control structures considered as operators of a data type.