• Volume 3,Issue 2,2009 Table of Contents
    Select All
    Display Type: |
    • >Special Double Issue on Formal Methods of Program Development
    • Editorial

      2009, 3(2):121-127.

      Abstract (3799) HTML (0) PDF 477.63 K (3147) Comment (0) Favorites

      Abstract:

    • Designing and Analyzing a Flash File System with Alloy

      2009, 3(2):129-148.

      Abstract (4985) HTML (0) PDF 3.29 M (3997) Comment (0) Favorites

      Abstract:Alloy is a lightweight modeling language based on .rst-order relational logic. The language is expressive enough to describe structurally complex systems, but simple enough to be amenable to fully automated analysis. The Alloy analyzer, with its SAT-based analysis engine, allows one to simulate traces of a system, visualize them, or search for counterexamples to a property. This article illustrates key concepts of Alloy using, as an example, the construction and analysis of a design for a .ash .le system. In addition to basic .le operations, the design includes features that are crucial to NAND .ash memory but contribute to increased complexity of the .le system, such as wear leveling and erase-unit reclamation. The design also addresses the issues of fault-tolerance by providing a mechanism for recovering from unexpected hardware failures. The article describes the modeling process and discusses the results of the design analysis, which has been carried out by checking trace inclusion of the .ash .le system against a POSIX-compliant abstract .le system.

    • Symbolic Bounded Model Checking of Abstract State Machines

      2009, 3(2):149-170.

      Abstract (4725) HTML (0) PDF 1.28 M (3814) Comment (0) Favorites

      Abstract:Abstract State Machines (ASMs) allow modeling system behaviors at any desired level of abstraction, including a level with rich data types, such as sets, sequences, maps, and user-de.ned data types. The availability of high-level data types allow state elements to be represented both abstractly and faithfully at the same time. In this paper we look at symbolic analysis of ASMs. We consider ASMs over a .xed state background T that includes linear arithmetic, sets, tuples, and maps. For symbolic analysis, ASMs are translated into guarded update systems called model programs. We formulate the problem of bounded path exploration of model programs, or the problem of Bounded Model Program Checking (BMPC) as a satis.ability problem modulo T . Then we investigate the boundaries of decidable and undecidable cases for BMPC. In a general setting, BMPC is shown to be highly undecidable (Σ11 -complete); and even when restricting to .nite sets the problem remains re-hard (Σ01-hard). On the other hand, BMPC is shown to be decidable for a class of basic model programs that are common in practice. We use Satis.ability Modulo Theories (SMT) for solving BMPC; an instance of the BMPC problem is mapped to a formula, the formula is satis.able modulo T if and only if the corresponding BMPC problem instance has a solution. The recent SMT advances allow us to directly analyze speci.cations using sets and maps with specialized decision procedures for expressive fragments of these theories. Our approach is extensible; background theories need in fact only be partially solved by the SMT solver; we use simulation of ASMs to support additional theories that are beyond the scope of available decision procedures.

    • Efficient Model Checking for Duration Calculus?

      2009, 3(2):171-196.

      Abstract (51635) HTML (0) PDF 3.39 M (4271) Comment (0) Favorites

      Abstract:Duration Calculus (abbreviated to DC) is an interval-based, metric-time tempo-ral logic designed for reasoning about embedded real-time systems at a high level of abstrac-tion. But the complexity of model checking any decidable fragment featuring both negation and chop, DC’s only modality, is non-elementary and thus impractical. Even worse, when such decidable fragments are generalized just slightly to cover more interesting durational constraints the resulting fragments become undecidable. We here investigate a similar approximation as frequently employed in model checking situation-or point-based temporal logics, where linear-time problems are safely approximated by branching-time counterparts amenable to more e.cient model-checking algorithms. Mim-icking the role that a situation has in (A)CTL as the origin of a set of linear traces, we de.ne a branching-time counterpart to interval-based temporal logics building on situation pairs spanning sets of intervals. While this branching-time interval semantics yields the desired reduction in complexity of the model-checking problem, from undecidable to linear in the size of the formula and cubic in the size of the model, the approximation is too coarse to be practical. We therefore re.ne the semantics by an occurrence count for crucial states (e.g., cuts of loops) in the model, arriving at a 4-fold exponential model-checking problem su.ciently accurately approximating the original one. Furthermore, when chop occurs in negative polarity only in DC formulas, we have a doubly exponential model-checking algo-rithm.

    • Refinement-Based Guidelines for Algorithmic Systems

      2009, 3(2):197-239.

      Abstract (4841) HTML (0) PDF 2.29 M (3451) Comment (0) Favorites

      Abstract:The correct-by-construction approach can be supported by a progressive and incremental process controlled by the re.nement of models of programs. We explore the EVENT B modelling language to illustrate the expression of our methodological proposal using proof-based patterns called guidelines. The main objective is to facilitate the correct-by-construction approach for designing classical sequential algorithms. We address the de-scription of guidelines for the design of programs and algorithms and the integration of proof-based aspects using the RODIN platform. More precisely, we introduce several method-ological steps identi.ed during the development of case studies, and we propose auxiliary notions, such as re.nement diagrams, for guiding users during problem analysis. A general structure characterizes the relationship between the contract, the EVENT B, and the devel-oped algorithm using a speci.c application of EVENT B models and re.nement. We simplify the translation of EVENT B models into algorithmic elements by promoting the use of recur-sive constructs. The resulting algorithm is proved to be sound with respect to the pre/post speci.cation, namely, the contract. Applications rely on a dynamic programming technique that illustrates the applicability of these patterns based on a call-as-event relationship. Each proof-based development is validated using the RODIN platform. Our paper contributes to the development of patterns for assisting the proof-based development of algorithmic systems.

    • Developing a Domain Model for Relay Circuits

      2009, 3(2):241-272.

      Abstract (3415) HTML (0) PDF 905.63 K (3533) Comment (0) Favorites

      Abstract:In this paper we stepwise develop a domain model for relay circuits as used in railway control systems. First we provide an abstract, property-oriented model of networks consisting of components that can be glued together with connectors. This model is strongly inspired by a network model for railways made by Bj.rner et. al., however our model is more general: the components can be of any kind and can later be re.ned to e.g. railway components or circuit components. Then we show how the abstract network model can be re.ned into an explicit model for relay circuits. The circuit model describes the statics as well as the dynamics of relay circuits, i.e. how a relay circuit can be composed legally from electrical components as well as how the components may change state over time. Finally the circuit model is transformed into an executable model, and we show how a concrete circuit can be de.ned, checked to be legal, and the reaction to an input can be simulated.

    • Formal Verification of a Consensus Algorithm in the Heard-Of ModelReal-Time Embedded Systems Using VDM

      2009, 3(2):273-303.

      Abstract (673) HTML (0) PDF 301.82 K (675) Comment (0) Favorites

      Abstract:Distributed algorithms are subtle and error-prone. Still, very few of them have been formally veri?ed, most algorithm designers only giving rough and informal sketches of proofs. We believe that this unsatisfactory situation is due to a scalability problem of current formal methods and that a simpler model is needed to reason about distributed algorithms. We consider formal veri?cation of algorithms expressed in the Heard-Of model recently introduced by Charron-Bost and Schiper. As a concrete case study, we report on the formal veri?cation of a non-trivial Consensus algorithm using the proof assistant Isabelle/HOL.

    • Methods for the Development of Distributed Real-Time Embedded Systems Using VDM

      2009, 3(2):305-341. DOI: 10.21655/ijsi.1673-7288.00305

      Abstract (5321) HTML (0) PDF 398.17 K (4645) Comment (0) Favorites

      Abstract:The development of distributed real-time embedded systems presents a signi?cant practical challenge both because of the complexity of distributed computation and because of the need to rapidly assess a wide variety of design alternatives in early stages when requirements are often volatile. Formal methods can address some of these challenges but are often thought to require greater initial investment and longer development cycles than is desirable for the development of non-critical systems in highly competitive markets. In this paper we propose an approach that takes advantage of formal modelling and analysis technology in a lightweight way, making signi?cant use of readily available tools. We describe an incremental approach in which detail is progressively added to abstract system-level speci?cations of functional and timing properties via intermediate models that express system architecture, concurrency and distribution. The approach is illustrated using a model of a home automation system. The models are expressed using the Vienna Development Method (VDM) and are validated primarily by scenario-based tests.

    • >Special Double Issue on Formal Methods of Program Development
    • The Application of VDM to the Industrial Development of Firmware for a Smart Card IC Chip

      2009, 3(2):343-355.

      Abstract (5234) HTML (0) PDF 736.78 K (4243) Comment (0) Favorites

      Abstract:We have applied the formal speci.cation language in the development of the .rmware of the smart card IC chip for embedding in mobile phone. We report on an in-dustrial application of formal methods to the development of a complex system, namely the .rmware for the “Mobile FeliCa” smart card IC chip. The use of formal techniques, specif-ically the Vienna Development Method (VDM), was aimed at raising the quality of system speci.cations by reducing ambiguity and improving communications between engineers. De-velopment data gathered during the life cycle con.rm the e.ectiveness of a lightweight formal method in contributing to the quality of the deliverables in early development stages. No software speci.cation problems have, to date, been reported since .rst release (over 100 million mobile phones have the chip embedded).

    • A Chain Datatype in Z

      2009, 3(2):357-374.

      Abstract (3301) HTML (0) PDF 901.95 K (3321) Comment (0) Favorites

      Abstract:We present results about a general-purpose chain datatype specified in the Z notation and mechanised using the Z/Eves theorem prover. Our particular interest comes from its use in the specification and refinement of operating system kernels for embedded real-time devices as part of a pilot project within the international Grand Challenge in Verified Software, and to contribute to the Verified Software Repository. We show—at afairly high level—the sort of dogged work that is needed to get a body of results together to form a basis for future projects. Our work discusses important hidden and missing properties in the specification of the chain datatype and its relation to kernel design.

    • Fault-Based Conformance Testing in Practice

      2009, 3(2):375-411.

      Abstract (3863) HTML (0) PDF 1.94 M (5045) Comment (0) Favorites

      Abstract:Conforming to protocol speci.cations is a critical issue in modern distributed software systems. Nowadays, complex service infrastructures, such as Voice-over-IP systems, are usually built by combining components of di.erent vendors. If the components do not correctly implement the various protocol speci.cations, failures will certainly occur. In the case of emergency calls this may be even life-threatening. Functional black-box conformance testing, where one checks the conformance of the implemented protocol to a speci.cation becomes therefore a major issue. In this work, we report on our experiences and .ndings when applying fault-based conformance testing to an industrial application. Besides a discussion on modeling and simpli.cations we present a technique that prevents an application from implementing particular faults. Faults are modeled at the level of the speci.cation. We show how such a technique can be adapted to speci.cations with large state spaces and present results obtained when applying our technique to the Session Initiation Protocol and to the Conference Protocol. Finally, we compare our results to random and scenario based testing.