Entiv Firmware Standard Practices Lightweight Analysis of Object Interactions Fourth International Symposium on Theoretical Aspects of Computer Software, Sendai, Japan, October 2001. The state of the practice in object-oriented software development has moved beyond reuse of code to reuse of conceptual structures such as design patterns. This paper draws attention to some difficulties that need to be solved if this style of development is to be supported by formal methods. In particular, the centrality of object interactions in many designs makes traditional reasoning less useful, since classes cannot be treated fruitfully in isolation from one another. We propose some ideas towards dealing with these issues: a relational model of heap structure capable of expressing sharing and mutual influence between objects; a declarative specification style that works in the presence of collaboration; and a tool-supported constraint analysis to expose problems in a diagram that captures, at a design level, a pattern of interaction. We illustrate these ideas with an example taken from a program used in the formatting of this paper.
A Micro modularity Mechanism Proc. ACM SIGSOFT Conf. Foundations of Software Engineering/European Software Engineering Conference (FSE/ESEC '01), Vienna, September 2001. A simple mechanism for structuring specifications is described. By modeling structures as atoms, it remains entirely first-order and thus amenable to automatic analysis. And by interpreting fields of structures as relations, it allows the same relational operators used in the formula language to be used for dereferencing. An extension feature allows structures to be developed incrementally, but requires neither textual inclusion nor any notion of sub typing. The paper demonstrates the flexibility of the mechanism by application in a variety of common idioms.
Object Models as Heap Invariants A chapter in: Essays on Programming Methodology, edited by Carroll Morgan and Annabelle McIver. Springer Verlag, 2000. Object models are widely used for describing structural properties of object-oriented programs, but they suffer from two problems. First, their semantics is usually unclear. Second, the textual constraints that are often used to annotate diagrams are not integrated with the diagrammatic notation itself. In this paper, we show how to interpret an object model as a heap invariant by translation to a small relational logic. With a few additional shorthands, this logic can be used for textual constraints, so that annotation is just conjunction. Our semantics is simpler than those proposed by others, and accounts for features of the object model that have not been addressed in treatments that focus on more abstract models.
Lecture Notes on Software Design Fall 2000 Lecture notes from 6.170: Laboratory in Software Engineering. Basic notions of object oriented programming, data abstraction, object models, dependences, etc. Object modeling used pervasively throughout, from describing the structure of the Java heap to analyzing conceptual models.
Automating First-Order Relational Logic Proc. ACM SIGSOFT Conf. Foundations of Software Engineering. San Diego, November 2000. An automatic analysis method for first-order logic with sets and relations is described. A first-order formula is translated to a quantifier-free Boolean formula, which has a model when the original formula has a model within a given scope (that is, involving no more than some finite number of atoms). Because the satisfiable formulas that occur in practice tend to have small models, a small scope usually suffices and the analysis is efficient. The paper presents a simple logic and gives a compositional translation scheme. It also reports briefly on experience using the Alloy Analyzer, a tool that implements the scheme.
COM Revisited: Tool Assisted Modeling and Analysis of Software Structures Proc. ACM SIGSOFT Conf. Foundations of Software Engineering. San Diego, November 2000 Designing architectural frameworks without the aid of formal modeling is error prone. But, unless supported by analysis, formal modeling is prone to its own class of errors, in which formal statements fail to match the designer’s intent. A fully automatic analysis tool can rapidly expose such errors, and can make the process of constructing and refining a formal model more effective. This paper describes a case study in which we recast a model of Microsoft COM’s query interface and aggregation mechanism into Alloy, a lightweight notation for describing structures. We used Alloy’s analyzer to simulate the specification, to check properties and to evaluate changes. This allowed us to manipulate our model more quickly and with far greater confidence than would otherwise have been possible, resulting in a much simpler model and a better understanding of its key properties.
Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer Proc. 15th IEEE International Conference on Automated Software Engineering, Grenoble, France, September 2000 Lightweight formal modeling and automatic analysis were used to explore the design of the Intentional Naming System (INS), a new scheme for resource discovery in a dynamic networked environment. We constructed a model of INS in Alloy, a lightweight relational notation, and analyzed it with Alcoa, a fully automatic simulation and checking tool. In doing so, we exposed several serious flaws in both the algorithm of INS and the underlying naming semantics. We were able to characterize the conditions under which the existing INS scheme works correctly, and evaluate proposed fixes.
Finding Bugs with a Constraint Solver International Symposium on Software Testing and Analysis, Portland, OR, August 2000 A method for finding bugs in code is presented. For given small numbers j and k, the code of a procedure is translated into a relational formula whose models represent all execution traces that involve at most j heap cells and k loop iterations. This formula is conjoined with the negation of the procedure's specification. The models of the resulting formula, obtained using a constraint solver, are counterexamples: executions of the code that violate the specification. The method can analyze millions of executions in seconds, and thus rapidly expose quite subtle flaws. It can accommodate calls to procedures for which specifications but no code is available. A range of standard properties (such as absence of null pointer dereferences) can also be easily checked, using predefined specifications.
Enforcing Design Constraints with Object Logic Static Analysis Symposium 2000, Santa Barbara, CA, June/July 2000 Springer Verlag, LNCS 1824 Design constraints express essential behavioral properties of a software system. Two key elements of a scheme for enforcing design constraints are presented: logic for describing the constraints, and an analysis that can be used both to explore the constraints in isolation (and thus gain confidence in their correctness), and to check that they are obeyed by an implementation. Examples of applications of the logic and its analysis at various levels of abstraction are given, from high-level designs to finding bugs in code. The challenge of bridging several levels, and checking code against abstract design constraints, is illustrated with a scenario from an air-traffic control system.
Alcoa: the Alloy Constraint Analyzer Proc. International Conference on Software Engineering, Limerick, Ireland, June 2000 Alcoa is a tool for analyzing object models. It has a range of uses. At one end, it can act as a support tool for object model diagrams, checking for consistency of multiplicities and generating sample snapshots. At the other end, it embodies a lightweight formal method in which subtle properties of behavior can be investigated. Alcoa's input language, Alloy, is a new notation based on Z. Its development was motivated by the need for a notation that is more closely tailored to object models (in the style of UML), and more amenable to automatic analysis. Like Z, Alloy supports the description of systems whose state involves complex relational structure. State and behavioral properties are described declaratively, by conjoining constraints. This makes it possible to develop and analyze a model incrementally, with Alcoa investigating the consequences of whatever constraints are given. Alcoa works by translating constraints to Boolean formulas, and then applying state-of-the-art SAT solvers. It can analyze billions of states in seconds.
The Future of Software Analysis A chapter in 'The Future of Software Engineering', editor Anthony Finkelstein, ACM Press, June 2000 We describe the challenges of software analysis by presenting a series of dichotomies. Each gives a spectrum on which any particular analysis can be placed; together, they give some structure to the space of possible analyses. Our intent is not, however, to provide a survey of existing analyses within this space, but to argue that some regions are more likely to be important in the future than others. Recognizing that our opinions do not represent the consensus of the community, we have tried, for each dichotomy, to make a case for both extremes (or at least identifying the contexts in which one makes more sense) while arguing primarily for one over the other. We argue that in the future analyses will be model-driven, namely centered on abstract models of behavior; modular and incremental, to enable analysis of components, and of systems before completion; and focused and partial, rather than uniform, paying closer attention to properties that matter most and to the parts of the software that affect those properties. In support of such analyses, we expect modeling languages to be global, with a focus on structural relationships across the system, and declarative, and we expect the analyses themselves to make more use of induction than has been fashionable recently. Finally, although we believe that unsound analyses have a bright future, we expect the increasing importance of infrastructural software to bring a renewed credibility to sound, precise and resource-intensive analyses.
Some Shortcomings of OCL, the Object Constraint Language of UML Response to Object Management Group's Request for Information on UML 2.0 December 1999 The purpose of this paper is to expose some shortcomings of the Object Constraint Language (OCL). We argue that, despite its numerous benefits, OCL is too implementation-oriented and therefore not well suited for conceptual modeling. Moreover, it is at times unnecessarily verbose, yet far from natural language. In the past couple of years, we have designed a language, Alloy that has similar motivations to OCL, while attempting to avoid some of these drawbacks. To illustrate the weaknesses of OCL, and some ways in which it may be improved, we have translated most of the core package of the UML metamodel, together with its well-formedness constraints, into Alloy. Moreover, we have shown that this subset of the UML metamodel is consistent, provided that this translation is valid, using Alloy's analysis tool, Alcoa.
Redesigning Air-Traffic Control: A Case Study in Software Design IEEE Software, May/June 2000 We redesigned and reimplemented a component of CTAS, an air traffic control system developed by NASA and now deployed in several US airports. Our case study demonstrates how basic software engineering techniques can make a complex system dramatically simpler. We describe lessons learned from reverse engineering the component with a variety of tools and redesigning it to be smaller, simpler and more flexible.
Alloy: A Lightweight Object Modeling Notation July 2000 Alloy is a little language for describing structural properties. It offers a declaration syntax compatible with graphical object models, and a set-based formula syntax powerful enough to express complex constraints and yet amenable to a fully automatic semantic analysis. It’s meaning is given by translation to an even smaller (formally defined) kernel. To make Alloy easy to use, a number of complications have been avoided: there are no tuples, no set or relation constants, and no undefined expressions or special null values. This paper presents the language in its entirety, and explains its motivation, contributions and deficiencies.
A Comparison of Object Modeling Notations: Alloy, UML and Z Unpublished manuscript. August 1999 An example of an object model is given in full in three languages: Alloy, a new notation; Z, a formal specification language; and UML, a modeling notation popular in industry. Basic features of Alloy are explained informally, and briefly justified by comparison of the Alloy version to the UML and Z versions.
An Intermediate Design Language and its Analysis Proc. ACM SIGOFT Conf. Foundations of Software Engineering, Orlando, FL, November 1998 A simple relational language is presented that has two desirable properties. First, it is sufficiently expressive to encode, fairly naturally, a variety of software design problems. Second, it is amenable to fully automatic analysis. This paper explains the language and its semantics, and describes a new analysis scheme (based on a stochastic Boolean solver) that dramatically outperforms existing schemes.
Lightweight Extraction of Object Models from Byte code IEEE Transactions on Software Engineering, February 2001 A program’s object model captures the essence of its design. For some programs, no ob-ject model was developed during design; for others, an object model exists but may be out-of-sync with the code. This paper describes a tool that automatically extracts an object model from the class files of a Java program. Unlike existing tools, it handles container classes, by inferring the types of elements stored in a container, and eliding the container itself. This feature is crucial for obtaining models that show the structure of the abstract state, and bear some relation to conceptual models. Although the tool performs only a simple, heuristic analysis that is almost entirely local, the resulting object model is surprisingly accurate. The paper explains what object models are and why they are useful; describes the analysis, its assumptions and limitations; evaluates the tool for accuracy, and illustrates its use, on a suite of sample programs.
Boolean Compilation of Relational Specifications Technical Report MIT-LCS-735, December 1997 A new method for analyzing relational specifications is described. A property to be checked is cast as a relational formula, which, if the property holds, has no finite models. The relational formula is translated into a Boolean formula that has a model for every model of the relational formula within some finite scope. Errors in specifications can usually be demonstrated with small counterexamples, so a small scope often suffices. An off-the-shelf satisfier solves the Boolean formula. The satisfier requires that the Boolean formula be in conjunctive normal form (CNF). A naive translation to CNF fails (by exhausting memory) for realistic specifications. This paper presents a preliminary design of a compiler that overcomes this problem, by exploiting typical features of the relational formulae that arise in practice. Initial experiments suggest that this method scales more readily than existing approaches and will be able to find more errors, in larger specifications.
Isomorphs-free Model Enumeration: A New Method for Checking Relational Specifications ACM Trans. Programming Languages and Systems, Vol. 20, No. 2, March 1998, pp. 302-343 Software specifications often involve data structures with huge numbers of values and consequently cannot be checked using standard state explosion or model checking techniques. Data structures can be expressed with binary relations and operations over such structures can be expressed as formulae involving relational variables. Checking properties such as preservation of an invariant thus reduces to determining the validity of a formula or, equivalently, finding a model of the formula's negation. A new method for finding relational models is presented. It exploits the permutation invariance of models--if two models are isomorphic, then neither is a model or both are--by partitioning the space into equivalence classes of symmetrical interpretations. Representatives of these classes are constructed incrementally by using the symmetry of the partial interpretation to limit the enumeration of new selection values. The notion of symmetry depends on the type structure of the formula: by picking the weakest typing larger equivalence classes (and thus fewer representatives) are obtained. A more refined notion of symmetry that exploits the meaning of the relational operators is also described. The method typically leads to exponential reductions: In combination with other simpler reductions it makes automatic analysis of relational specifications possible for the first time.
A Nitpick Analysis of Mobile IPv6 To appear, Formal Aspects of Computing A lightweight formal method enables partial specification and automatic analysis by sacrificing breadth of coverage and expressive power. By design, NP is a specification language that is a subset of Z and Nitpick is a tool that quickly and automatically checks properties of finite models of systems specified in NP. We used NP to state two critical acyclicity properties of Mobile IPv6, a new internetworking protocol that allows mobile hosts to communicate with each other. In our Nitpick analysis of Mobile IPv6 we discovered a flaw in a 1996 version of the design: one of the acyclicity properties does not hold. It takes only two hosts to exhibit this flaw. This paper gives self-contained overviews of Mobile IPv6 and of NP and Nitpick to understand the details of our specification and analysis.
Faster Checking of Software Specifications By Eliminating Isomorphs Both software specifications and their intended properties can be expressed in a simple relational calculus. The claim that a specification satisfies a property becomes a relational formula that can be checked automatically by enumerating the formula's interpretations. Because the number of interpretations is usually huge, this approach has not been thought to be practical. But by eliminating isomorphic interpretations, the enumeration can be reduced substantially, by a factor of k! For each basic type of k elements.
Automatic Analysis of Architectural Style Unpublished manuscript A new technique for analyzing architectural styles is presented. The style is specified in NP, a relational notation similar to Z, along with properties expected to hold for all instances of the style. The specification is checked by Nitpick, a fully automatic checker for NP. Nitpick exhaustively enumerates all instances of the style-that is, all architectures that conform to the style-within given finite bounds, and reports those instances that fail to satisfy the expected properties. The technique is applied to a specification of a family of implicit invocation styles developed originally in Z by Garlan and Notkin. The analysis exposes some potential trouble spots, highlights differences between the styles, and suggests some refinements.
Abstract Model Checking of Infinite Specifications Proc. Formal Methods Europe, Barcelona, October 1994 A new method for analyzing specifications in languages like Z and VDM is proposed. Theorems are checked automatically by exhaustive search of the state space. An abstraction over the actual states can be defined that reduces an infinite state space to a finite number of equivalence classes, allowing it to be searched exhaustively by treating each class as a single abstract state. A prototype has been built that has verified some small theorems from the literature.
Lackwit: Large-Scale Analysis of C Programs Using Polymorphic Type Inference Many software engineering tasks require information about whole programs, but available tools either do not scale to handle problems of large size and complexity or provide only superficial information. We have developed a fully automatic tool, Lackwit, that can answer many kinds of queries about C programs (for example, "locate all potential assignments to this field"), taking into account the effects of pointer aliasing, calls through function pointers, and type casts. The analysis is based on the kind of type inference developed for functional languages, but uses enriched types as abstractions of program functions and variables. It is simple and modular, and surprisingly accurate in practice. It can answer queries about a Linux 2.0 kernel (187,000 lines) in under ten minutes on a modestly equipped PC. In this paper, we describe the theory of the analysis, its realization when applied to C programs, how the tool presents the results of the analysis to the user, and the results of our experiments.
A New Model of Program Dependences for Reverse Engineering Proc. SIGSOFT Conf. on Foundations of Software Engineering, New Orleans, December 1994 A dependence model for reverse engineering should treat procedures in a modular fashion and should be fine-grained, distinguishing dependences that are due to different variables. The program dependence graph (PDG) satisfies neither of these criteria. We present a new form of dependence graph that satisfies both, while retaining the advantages of the PDG: it is easy to construct and allows program slicing to be implemented as a simple graph traversal. We define 'chopping', a generalization of slicing that can express most of its variants, and show that, using our dependence graph, and it produces more accurate results than algorithms based directly on the PDG.
Problem Decomposition for Reuse Software Engineering Journal, Vol. 11, No. 1, January 1996 An approach to software development problems is presented, and illustrated by an example. The approach is based on the ideas of problem frames and structuring specifications by views. It is claimed that decompositions obtained by this approach result in a more effective separation of concerns, and that the resulting components are more likely to be reusable than those obtained by more conventional approaches. The characteristics of desirable integration mechanisms are discussed, together with some other considerations arising out of the approach presented.
Structuring Z Specifications With Views ACM Trans. on Software Engineering and Methodology, Vol. 4, No. 4, October 1995 A view is a partial specification of a program, consisting of a state space and a set of operations. A full specification is obtained by composing several views, linking them through their states (by asserting invariants across views) and through their operations (by defining external operations as combinations of operations from different views). By encouraging multiple representations of the program's state, view structuring lends clarity and terseness to the specification of operations. And by separating different aspects of functionality, it brings modularity at the grossest level of organization, so that specifications can accommodate change more gracefully. View structuring in Z is demonstrated with a few small examples. Both the features of Z that lend themselves to view structuring, and those that are a hindrance, are discussed examples. Both the features of Z that lend themselves to view structuring, and those that are a hindrance, are discussed.
Lightweight Formal Methods IEEE Computer, April 1996
|