Search

We present αRby--an embedding of the Alloy language in Ruby--and demonstrate the benefits of having a declarative modeling language backed by an automated solver embedded in a traditional object-oriented imperative programming language. This approach aims to bring these two distinct paradigms imperative and declarative together in a novel way. We argue that having the other paradigm available within the same language is beneficial to both the modeling community of Alloy users and the object-oriented community of Ruby programmers. In this paper, we primarily focus on the benefits for the Alloy community, namely, how αRby provides elegant solutions to several well-known, outstanding problems: 1 mixed execution, 2 specifying partial instances, 3 staged model finding.

How should a software system be verified? Much research is currently focused on attempts to show that code modules meet their specifications. This is important, but bugs in code are not the weakest link in the chain. The larger problems are identifying and articulating critical properties, and ensuring that the components of a system - not only software modules, but also hardware peripherals, physical environments, and human operators - together establish them. Another common assumption is that verification must take system design and implementation as given. I’ll explain the rationale for, and elements of, a new approach to verification, in which design is driven by verification goals, and verification arguments are structured in a way that exposes the relationship between critical properties and the components that ensure them.

We extend the Alloy language with the standard imperative constructs; we show the mix of declarative and imperative constructs to be useful in modeling dynamic systems. We present a translation from our extended language to the existing first-order logic of the Alloy Analyzer, allowing for efficient analysis of models.

This paper describes a pedagogical pattern for cross-cultural language learning and its application in a case study involving learners in Australia and China. The pattern uses a multimedia discussion tool as its main component, supported by video conferencing and chat. We analyze how students interacted with the tools, especially the documents they created and the commenting behavior. Based on this analysis, we give a set of recommendations relevant to practitioners and researchers in technology-enhanced language learning.

As the exact pain measurement is an important prerequisite for pain management, this work aims to measure Pain objectively. As the physiological parameters have significant relationship with pain, we intend to measure ECG, HR, BP and GSR with the equal amount of pain being induced on all the subjects. For this purpose, we have designed an apparatus called Pain Inducer which consists of five discs mounted on a central slot to induce the pain. The experiments (Pre Pain, During Pain and Post pain experiments) were conducted inside the controlled laboratory environment. The parameters have been acquired and analyzed by an instrument called physiograph (RMS Polyrite-D). We have chosen 50 male volunteers of age between 20 and 22 years, for this purpose. The subjects were with normal appetite (food habits) and residing in a confined locality. It is found that both the cardiac parameters and somatic resistance showed significant changes between the ‘pain’ and ‘ no pain’ conditions. However more experimental studies with additional physiological parameters on large number of subjects in actual clinical setup are required to validate this method. Also, a generalized pain measurement system for all kinds of pain is another challenge to be addressed. Further work on this area may improve the utility of this method in clinical practices for measuring pain objectively. It leads to reduced administration of painkillers.

Great progress has been made in software verification. One has only to look, for example, at the growth in power of SAT and its widening class of applications to realize that concerns early on that verification was fundamentally intractable and that it would remain a largely manual activity were mistaken. Nevertheless, despite many research advances, verification is still not widely applied to software. In order to make verification practical, some fundamental obstacles will need to be addressed. This talk outlined a sample of these obstacles, in three categories: technical obstacles in the mechanism of verification itself; engineering obstacles related to the problem of establishing confidence in a system rather than a single component; and social and managerial obstacles related to the process of verification. These obstacles are known and have been fairly widely discussed. It is useful, however, to remind ourselves of them since otherwise, as a research community, we risk focusing on technical details that may be overwhelmed by these larger factors. In explaining some of the obstacles, I also sought to question some assumptions that are often made in the verification community that make sense in a narrower, mathematical context but are not defensible in the larger system context. One example of this is the notion of conservatism. It is often assumed that a 'conservative' analysis that never misses bugs, but which may generate false alarms, is necessarily superior to an analysis that is 'unsound' and may fail to report real errors. In practice, however, this superiority is not inevitable, and in many cases, an unsound analysis is preferable. First, the need to be conservative can result in a dramatic increase in false positives, so that the unsound analysis may actually be more accurate (in the sense that the probability of missing a bug is low, whereas the comparable conservative analysis produces a report full of erroneous claims). Second, the presence of false alarms may increase the burden of reading the report so dramatically that bugs may be overlooked in the filtering process, so that the conservative analysis becomes, in its context of use, unsound. Similarly, in a software design context, the assumption that checks should be conservative is often not justified in engineering terms. In air-traffic control, for example, it has long been recognized that a conflict detection tool must not generate false alarms. The catastrophic accident in Guam in 1997, in which a 747 flew into the ground, might not have occurred had a safe-altitude-warning system not been disabled because of its over-conservative error reporting.

We present a case-study in which vote-tallying software is analyzed using a bounded verificationtechnique, whereby all executions of a procedure are exhaustively examined within a finite space given by a bound on the size of the heap and the number of loop unrollings. The technique involves an encoding of the procedure in an intermediate relational programming language, a translation of that language to relational logic, and an analysis of the logic that exploits recent advances in finite model-finding. Our technique yields concrete counterexamples --- traces of the procedure that violate the specification. The vote-tallying software, used for public elections in the Netherlands, had previously been annotated with specifications in the Java Modeling Language and analyzed with ESC/Java2. Our analysis found counterexamples to the JML contracts, indicating bugs in the code and errors in the specifications that evaded prior analysis.

This paper describes the formal modeling and analysis of a design for a flash-based filesystem in Alloy. We model the basic operations of a filesystem as well as features that are crucial to NAND flash hardware, such as wear-leveling and erase-unit reclamation. In addition, we address the issue of fault tolerance by modeling a mechanism for recovery from interrupted filesystem operations due to unexpected power loss. We analyze the correctness of our flash filesystem model by checking trace inclusion against a POSIX-compliant abstract filesystem, in which a file is modeled simply as an array of data elements. The analysis is fully automatic and complete within a finite scope.

Declarative specifications exhibit a variety of problems, such as inadvertently overconstrained axioms and underconstrained conjectures, that are hard to diagnose with model checking and theorem proving alone. Recycling core extractionis a new coverage analysis that pinpoints an irreducible unsatisfiable core of a declarative specification. It is based on resolution refutation proofs generated by resolution engines, such as SAT solvers and resolution theorem provers. The extraction algorithm is described, and proved correct, for a generalized specification language with a regulartranslation to the input logic of a resolution engine. It has been implemented for the Alloy language and evaluated on a variety of specifications, with promising results.

The key design challenges in the construction of a SAT-based relational model finder are described, and novel techniques are proposed to address them. An efficient model finder must have a mechanism for specifying partial solutions, an effective symmetry detection and breaking scheme, and an economical translation from relational to boolean logic. These desiderata are addressed with three new techniques: a symmetry detection algorithm that works in the presence of partial solutions, a sparse-matrix representation of relations, and a compact representation of boolean formulas inspired by boolean expression diagrams and reduced boolean circuits. The presented techniques have been implemented and evaluated, with promising results.

Often, a requirements document is structured as a long list of individual ”requirements”, each describing an anticipated function or user interaction. An alternative approach is to identify a collection of subproblems, each representing an aspect of the larger problem, and to describe each subproblem in isolation, deferring their composition to a later stage. This paper illustrates the approach by applying it to the requirements of the positioning functions of a proton therapy installation. It explains how a flaw in the design of the system can be isolated to a single subproblem, which can be formalized and subjected to automatic analysis.

Most modeling languages embody a particular idiom: the state/invariant/operations idiom for VDM and Z; the variable-update/temporal-logic idiom for SMV and Murphi; the imperative-programming idiom for Promela and Zing; and so on. Fixing an idiom makes tools easier to build, and helps novice modellers. But it also makes the language less flexible.

A new model of inter-module dependences is proposed. The key idea is that dependences are mediated by specifications, so that not only the existence of a dependence is recorded, but also its quality. A single module does not necessarily offer only a single specification; each dependent module may use it through a different specification. This notion of dependence seems to explain some common programming idioms more readily than the conventional notion, and offers new opportunities for analysis and design critique.

This paper describes the analysis of Pull-Based Asynchronous Rekeying Framework (ARF), a recently proposed solution to the scalable group key management problem in secure multicast. A model of this protocol is constructed in Alloy, a lightweight relational modeling language, and analyzed using the Alloy Analyzer, a fully automatic simulation and checking tool for Alloy models. In this analysis, some critical correctness properties that should be satisfied by any secure multicast protocol are checked. Some flaws, previously unknown to the protocol’s designers are exposed, including one serious security breach. To eliminate the most serious flaw, some fixes are proposed and checked using the Alloy Analyzer. The case study also illustrates a novel modeling idiom that supports better modularity and is generally simpler and more intuitive than the conventional idiom used for modeling distributed systems.

The software implementation of the emergency shutdown feature in a major radiotherapy system was analyzed, using a directed form of code review based on module dependences. Dependences between modules are labelled by particular assumptions; this allows one to trace through the code, and identify those fragments responsible for critical features. An ‘assumption tree’ is constructed in parallel, showing the assumptions which each module makes about others. The root of the assumption tree is the critical feature of interest, and its leaves represent assumptions which, if not valid, might cause the critical feature to fail. The analysis revealed some unexpected assumptions that motivated improvements to the code.

Alloy, like Z, is a language for modelling software systems. Indeed, it draws many of its good ideas from Z: in particular, representing all data structures with sets and relations, and representing behaviour and properties with simple formulas. Unlike Z, however, Alloy was designed with automatic analysis in mind. A constraint solver based on reduction to SAT can check properties of Alloy models, and simulate execution (even of implicit operations). The key idea is to consider all possible bindings of a formula that assign no more than some small number of atoms to each given type. The result is a flexible mechanism that provides rapid and concrete feedback during evolution of a model. It cannot prove properties, but by exhausting all small test cases, it usually succeeds in finding bugs rapidly. In my talk, I'll explain the fundamental ideas underlying Alloy and its analysis: its basis in relation rather than sets, and the compromises (notably a restriction to first order structures and formulas) that make analysis possible. I'll compare Alloy's specification-structuring mechanism, the signature, to Z's schema. I'll illustrate some modelling idioms that we have developed in using Alloy, focusing on how mutation is represented. I'll also show some examples of typical analyses, including a trace-based analysis that employs the idea of 'machine diameter' from bounded model checking to ensure that all reachable states are considered.

A method for finding bugs in object-oriented code is presented. It is capable of checking complex user-defined structural properties - that is, of the configuration of objects on the heap - and generates counterexample traces with no false alarms. It requires no annotation beyond the specification to be checked, and is fully automatic. The method relies on a three-step translation: from code to a formula in a first-order relational logic, then to a propositional formula, and finally to conjunctive normal form. An off-the-shelf SAT solver is then used to find a solution that constitutes a counter example. This underlying scheme, presented previously, does not scale readily. In this paper, we show how a suite of optimizations results in much improved scalability. The optimizations are based on a special treatment of relations that are known to be functional, and target all steps. The effect of the optimizations is demonstrated by application to the analysis of a red-black tree implementation.

Alloy is a lightweight language for software modelling. It's designed to be flexible and expressive, and yet amenable to fully automatic simulation and checking. At its core, Alloy is a simple first order logic extended withrelational operators. A simple structuring mechanism allows Alloy to be used in a variety of idioms, and supports incremental construction of models. Alloy is analyzed by translation to SAT. The current version of the tool uses the Chaff and Berkmin solvers; these are powerful enoughto handle a searchspace of 2100 or more. Alloy has been applied to problems from very different domains, from checking the conventions of Microsoft COM to debugging the design of a name server. Most recently, we have used it to check distributed algorithms that are designed for arbitrary topologies. We are also investigating the use of Alloy to analyze object-oriented code.

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.

Formal methods have offered great benefits, but often at a heavy price. For everyday software development, in which the pressures of the market don't allow full-scale formal methods to be applied, a more lightweight approach is called for. I'll outline an approach that is designed to provide immediate benefit at relatively low cost. Its elements are a small and succinct modelling language, and a fully automatic analysis scheme that can perform simulations and find errors. I'll describe some recent case studies using this approach, involving naming schemes, architectural styles, and protocols for networks with changing topologies. I'll make some controversial claims about this approach and its relationship to UML and traditional formal specification approaches, and I'll barbeque some sacred cows, such as the belief that executability compromises abstraction.

Design constraints express essential behavioural properties of a software system. Two key elements of a scheme for enforcing design constraints are presented: a 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.

The utility of directly executing formal specifications is briefly touched upon and the concept of exhaustive search as a means of execution is introduced. A mechanism for improving the efficiency of such searches is presented in some detail. Finally, the results of an implementation of the mechanism are presented.

There is an increasing demand for application-specific software. For example, the software to control a machine on a factory floor is different from the software to manipulate large databases. The software engineer building software to control a motor that powers a piece of machinery needs some understanding of the motor''s servo system; whereas a software engineer who designs the software to manage large databases for the NASA Space Station needs specific knowledge about database models as well as the types of data handled on a long-term space vehicle. Specialization tracks within the Master of Software Engineering (MSE) Program at Carnegie Mellon University would enable students to gain application knowledge while developing fundamental software engineering skills. This report proposes a model for establishing specialization tracks within a graduate software engineering program.

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.