Alloy is a well-known, formal, declarative language for modelling systems early in the software development process. Currently, it uses the K<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">odkod</small> library as a back-end for finite model finding. K<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">odkod</small> translates the model to a SAT problem; however, this method can often handle only problems of fairly low-size sets and is inherently finite. We present P<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">ortus</small>, a method for translating Alloy into an equivalent many-sorted first-order logic problem (MSFOL). Once in MSFOL, the problem can be evaluated by an SMT-based finite model finding method implemented in the F<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">ortress</small> library, creating an alternative back-end for the A<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">lloy</small> A<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">nalyzer</small>. F<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">ortress</small> converts the MSFOL finite model finding problem into the logic of uninterpreted functions with equality (EUF), a decidable fragment of first-order logic that is well-supported in many SMT solvers. We compare the performance of P<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">ortus</small> with K<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">odkod</small> on a corpus of 63 Alloy models written by experts. Our method is fully integrated into the A<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">lloy</small> A<sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">nalyzer</small>.

Modeling of software-intensive systems using formal declarative modeling languages offers a means of managing software complexity through the use of abstraction and early identification of correctness issues by formal analysis. Alloy is one such language used for modeling systems early in the development process. Little work has been done to study the styles and techniques commonly used in Alloy models. We present the first static analysis study of Alloy models. We investigate research questions that examine a large corpus of 1,652 Alloy models. To evaluate these research questions, we create a methodology that leverages the power of ANTLR pattern matching and the query language XPath. Our research questions are split into two categories depending on their purpose. The Model Characteristics category aims to identifywhatlanguage constructs are used commonly. Modeling Practices questions are considerably more complex and identifyhowmodelers are using Alloy's constructs. We also evaluate our research questions on a subset of models from our corpus written by expert modelers. We compare the results of the expert corpus to the results obtained from the general corpus to gain insight into how expert modelers use the Alloy language. We draw conclusions from the findings of our research questions and present actionable items for educators, language and environment designers, and tool developers. Actionable items for educators are intended to highlight underutilized language constructs and features, and help student modelers avoid discouraged practices. Actionable items aimed at language designers present ways to improve the Alloy language by adding constructs or removing unused ones based on trends identified in our corpus of models. The actionable items aimed at environment designers address features to facilitate model creation. Actionable items for tool developers provide suggestions for back-end optimizations.

Symmetry in finite model finding problems of many-sorted first-order logic (MSFOL) can be exploited to reduce the number of interpretations considered during search, thereby improving solver performance for tools such as the Alloy Analyzer. We present a framework to soundly compose static symmetry breaking schemes for many-sorted finite model finding. Then, we introduce and prove the correctness of three static symmetry breaking schemes for MSFOL: 1) one for functions with distinct sorts in the domain and range; 2) one for functions where the range sort appears in the domain; and 3) one for predicates. We provide a novel presentation of sort inference in the context of symmetry breaking that yields a new mathematical link between sorts and symmetries. We empirically investigate how our symmetry breaking approaches affect solving performance.

We address the problem of how to extract counterexamples for the transitive-closure-based model checking (TCMC) technique. TCMC is a representation of the CTLFC (CTL with fairness constraints) model checking problem in first-order logic with transitive closure (FOLTC) and has been implemented in the Alloy Analyzer. It is a declarative, symbolic model checking method. As a CTL model checking method, TCMC is defined over transition systems and states (rather than paths) and therefore, returns a transition system with a bug as a counterexample. Our contribution is to isolate a counterexample path/subgraph in a declarative manner by adding constraints that do not depend on the property. Our method does not require extensions to Alloy.

The feature interaction problem appears in many different kinds of complex systems, especially systems whose elements are created or maintained by separate entities - for example, a modern automobile that incorporates electronic systems produced by different suppliers. Cross-cutting concerns, such as safety and security, require a comprehensive analysis of the possible interactions. However, there is a combinatorial explosion in the number of feature combinations to be considered. Our work approaches the feature interaction problem from a novel point of view: we seek to use the abstract subject matter knowledge of domain experts to deduce why some features will NOT interact, rather than trying to discover or resolve the interactions. In this paper, we present a method that can automatically reduce the required number of combinations and situations that have to be evaluated or resolved for feature interactions. Our tool, called Morse, rules out feature combinations that cannot have interactions based on traceable deductions from relatively simple abstract requirements that capture relevant subject matter knowledge. Our method is useful as a means of focusing attention on particular situations where more detailed functional requirements may be needed to avoid unacceptable risk arising from unintended interactions between features. relatively simple abstract requirements that capture relevant subject matter knowledge. Our method is useful as a means of focusing attention on particular situations where more detailed functional requirements may be needed to avoid unacceptable risk arising from unintended interactions between features.

We motivate and present a proposal for how to represent the syntax of behavioural models written in extended finite-state machine languages with hierarchical states (e.g., the Statecharts family) in SMT-LIB. By including the state structure explicitly in the SMT-LIB model, our goal is to facilitate effective automated deductive reasoning, which can exploit the structure found in the state hierarchy. We present a novel method that combines deep and shallow encoding techniques to describe models that have both state hierarchy and use the rich datatypes found in SMT-LIB. Our representation permits varying semantics to be chosen for the syntax recognizing the rich variety of semantics that exist for this family of modelling languages. We hope that discussion of these representation issues will facilitate model sharing for investigation of analysis techniques.

Temporal logic model checking of infinite state systems without the use of iteration or abstraction is usually considered beyond the realm of first-order logic (FOL) reasoners because of the need for a fixpoint computation. In this paper, we show that it is possible to reduce model checking of a finite or infinite Kripke structure that is expressed in FOL to a validity problem in FOL for a fragment of computational tree logic (CTL), which we call CTL-live. CTL-live includes the CTL connectives that are traditionally used to express liveness properties. Our reduction can form the basis for methods that use FOL reasoning techniques directly to accomplish model checking of CTL-live properties without the need for fixpoint operators, transitive closure, abstraction, or induction.

The ability to create and analyze abstract models is an important step in conquering software complexity. In this paper, we show that it is practical to verify dynamic properties of infinite state models expressed in a subset of CTL directly using an SMT solver without iteration, abstraction, or human intervention. We call this subset CTL-Live and it consists of the operators of CTL expressible using the least fixed point operator of the mu-calculus, which are commonly considered liveness properties (e.g., AF, AU). We show that using this method the verification of an infinite state model can sometimes complete more quickly than verifying a finite version of the model. We also examine modelling techniques to represent abstract models in first-order logic that facilitate this form of model checking.

Avestan is a declarative modelling language compatible with SMT-LIB. SMT-LIB is an standard input language that is supported by the state-of-the-art satisfiability modulo theory solvers (SMT solvers). The recent advances in SMT solvers have introduced them as efficient analysis tools; as a result, they are becoming more popular in the verification and certification of digital products. SMT-LIB was designed to be machine readable rather than human readable. In this paper, we present Avestan, a declarative modelling language that is intended to be analyzed by SMT solvers and readable by humans. An Avestan model is translated to an SMT-LIB model so that it can be analyzed by different SMT solvers. Avestan has relational constructs that are heavily inspired by Alloy; we added these constructs to increase the readability of an Avestan model.

We show how static properties of declarative models can be efficiently analyzed in a symbolic model checker; in particular, we use Cadence SMV to analyze Alloy models by translating Alloy to SMV. The computational paths of the SMV models represent interpretations of the Alloy models. The produced SMV model satisfies its LTL specifications if and only if the original Alloy model is inconsistent with respect to its finite scopes; counterexamples produced by the model checker are valid instances of the Alloy model. Our experiments show that the translation of many frequently used constructs of Alloy to SMV results in optimized models such that their analysis in SMV is much faster than in the Alloy Analyzer. Model checking is faster than SAT solving for static problems when an interpretation can be eliminated by early decisions in the model checking search.

With the popularity of model-driven methodologies, and the abundance of modelling languages, a major question for a requirements engineer is: which language is suitable for modelling a system under study? We address this question from a semantic point-of-view for big-step modelling languages (BSMLs). BSMLs are a class of popular behavioural modelling languages in which a model can respond to an input by executing multiple, possibly concurrent, transitions. We deconstruct the operational semantics of a large class of BSMLs into high-level, orthogonal semantic aspects, and analyze the relative advantages and disadvantages of the common semantic options for each of these aspects. Our goal is to empower a requirements engineer to compare and choose an appropriate BSML.

We propose to use model checking to detect feature interactions in a set of features under design for an automotive embedded system. In this paper, we present (1) the characteristics of the feature interaction problem in the automotive domain that make model checking an appropriate detection technique; (2) our proposal for a general, systematic definition of feature interactions for this domain based on the set of actuators in the vehicle influenced by the features; and (3) our solutions to two modelling issues that arise when creating a description in SMV of the behaviour of an integrated set of automotive features designed in MATLAB's STATEFLOW.

Many distributed systems using IP-based communication protocols consist of chains of components that run concurrently and communicate asynchronously with their neighbours through ports. We present a compositional reasoning method using model checking and theorem proving to verify liveness properties of a communication protocol for chains of connections consisting of an unknown number of components. We outline how our method is used to verify properties of the call protocol of AT&T's Distributed Feature Composition (DFC) architecture.

Specifiers must be able to understand and compare the specification notations that they use. Traditional means for describing notations' semantics (e.g., operational semantics, logic, natural language) do not help users to identify the essential differences among notations. Previously, we presented a template-based approach defining model-based notations, in which semantics that are common among notations (e.g., the concept of an enabled transition) are captured in the template and a notation's distinct semantics (e.g., which states can enable transitions) are specified as parameters. We demonstrate the template's generality by using it to document the semantics of SCR, SDL, and Petri nets. We also show how the template can be used to compare notation variants. We believe template definitions of notations ease a user's effort in understanding and comparing model-based notations.

We propose a template-based approach to structuring the semantics of model-based specification notations. The basic computation model is a nonconcurrent, hierarchical state-transition machine (HTS), whose execution semantics are parameterized. Semantics that are common among notations (e.g., the concept of an enabled transition) are captured in the template, and a notation's distinct semantics (e.g., which states can enable transitions) are specified as parameters. The template semantics of composition operators define how multiple HTSs execute concurrently and how they communicate and synchronize with each other by exchanging events and data. The definitions of these operators use the template parameters to preserve notation-specific behavior in composition. Our template is sufficient to capture the semantics of basic transition systems, CSP, CCS, basic LOTOS, a subset of SDL88, and a variety of statecharts notations. We believe that a description of a notation's semantics using our template can be used as input to a tool that automatically generates formal analysis tools.

We propose a unifying framework for model-based specification notations. Our framework captures the execution semantics that are common among model-based notations, and leaves the distinct elements to be defined by a set of parameters. The basic components of a specification are non-concurrent state-transition machines, which are combined by composition operators to form more complex, concurrent specifications. We define the step-semantics of these basic components in terms of an operational semantics template whose parameters specialize both the enabling of transitions and transitions' effects. We also provide the operational semantics of seven composition operators, defining each as the concurrent execution of components, with changes to their shared variables and events to reflect inter-component communication and synchronization; the definitions of these operators use the template parameters to preserve in composition notation-specific behaviour. By separating a notation's step-semantics from its composition and concurrency operators, we simplify the definitions of both. Our framework is sufficient to capture the semantics of basic transition systems, CSP, CCS, basic LOTOS, ESTELLE, a subset of SDL88, and a variety of statecharts notations. We believe that a description of a notation's semantics in our framework can be used as input to a tool that automatically generates formal analysis tools.