6th International Conference, AMAST'97 Sydney, Australia, December13–17, 1997 Proceedings
This paper has developed a general model for software versioning and configuration, based on information systems. The set of versions of a module, called its version space, should form an information system. Depending on the development process of that module, different kinds of version space can be defined, and approximable mappings can be used to relate the different version spaces of a single module...
Tactics are commands used to guide goal-directed proofs in interactive proof environments. This paper presents various possible simplifications on tactic expression and provides a justification for these simplifications, based on a precise description of the way tactics operate. In particular, this paper introduces a class of head-oriented tactics that are especially suited for simplification. Most...
The axioms of iteration 2-theories capture the equational properties of iteration in conjunction with horizontal and vertical composition in all algebraically complete categories. We give a concrete representation of the free iteration 2-theory generated by a 2-signature.
We present an algebraic approach to the model checking of fault-tolerant systems. Fault models and fault-handling mechanisms are modelled using special-purpose process operators. Besides providing for natural models, special-purpose operators allow systems with large state spaces to be verified using systems with small state spaces. To support this verification technique we show that a kind of simulation...
This article presents an approach for the verification of communication properties in large-scale real-world embedded systems by means of formal methods. It is illustrated by examples and results obtained during an industrial verification project performed for a fault-tolerant system designed and implemented by Daimler-Benz Aerospace for the International Space Station ISS. The approach is based on...
A structural operational semantics of a non trivial sublanguage of Java is presented. This language includes dynamic creation of objects, blocks, and synchronization of threads. First we introduce a simple operational description of the sequential part of the language, where the memory is treated as an algebra with suitably axiomatized operations. Then, the interaction between threads via a shared...
This paper presents a permissive subsorted partial logic used in the CoFI Algebraic Specification Language. In contrast to other ordersorted logics, subsorting is not modeled by set inclusions, but by injective embeddings allowing for more general models in which subtypes can have different data type representations. Furthermore, there are no restrictions like monotonicity, regularity or local filtration...
We present a methodology for describing timing constraints within various time models. This methodology exploits the constraint-based modelling style available within Circal, a process algebra that permits a natural representation of time without any ad hoc extension. The methodology is illustrated through several examples in the area of communication protocols and asynchronous hardware.
We consider the problem of verifying properties in processes with durational actions. The properties are expressed in terms of a discrete-time extension of ACTL. The algorithm for model checking formulae in this logic over finite state timed transition systems is provided. We consider processes that have infinite models due to the increase of the value of the clock and show how to reduce the verification...
We define a hierarchy of compositional formal semantics of algebraic polynomial systems over F-algebras by abstract interpretation. This generalizes classical formal language theoretical results and contextfree grammar flow-analysis algorithms in the same uniform framework of universal algebra and abstract interpretation.
In this paper we show that formal program development can be viewed as a process of model building. Refinement diagrams are introduced and formally defined in terms of refinement developments. Hierarchical models are shown to be equivalent to modular refinement developments. Modular refinement developments are a subset of refinement developments and refinement diagrams. A function is defined to extract...
Our concern is the high level specification of reactive software systems such as information systems. We adopt an object oriented, temporal logic based approach to specification. The notion of transaction incorporates various application domains, for instance transactions as abstractions from processes as known from refinement theory, transactions as abstractions from business processes as known in...
Rether is a software-based real-time ethernet protocol developed at SUNY Stony Brook. The purpose of this protocol is to provide guaranteed bandwidth and deterministic, periodic network access to multimedia applications over commodity ethernet hardware. It has been implemented in the PreeBSD 2.1.0 operating system, and is now being used to support the Stony Brook Video Server (SBVS), a low-cost, ethernet...
We present several formal program refinement rules for designing multi-tasking programs with hard real-time constraints.
The high-quality modeling experiences embedded in the more mature graphical OO methods (OOMs) makes their application to complex systems attractive, but the lack of firm semantic bases for the modeling notations can significantly hamper the development of such systems. One approach to making OOMs more precise and amenable to rigorous analysis is to integrate them with suitable formal modeling techniques...
Completeness in abstract interpretation is an ideal and rare situation where the abstract semantics is able to take full advantage of the power of representation of the underlying abstract domain. In this paper, we develop an algebraic theory of completeness in abstract interpretation. We show that completeness is an abstract domain property and we prove that there always exist both the greatest complete...
Since they often embody compact but mathematically sophisticated algorithms, operations for computing the common transcendental functions in floating point arithmetic seem good targets for formal verification using a mechanical theorem prover. We discuss some of the general issues that arise in verifications of this class, and then present a machine-checked verification of an algorithm for computing...
An assertional method to verify distributed real-time and fault-tolerant protocols is presented. To obtain mechanical support, the verification system PVS is used. General PVS theories are developed to deal with timing and failures. As a characteristic example, we verify a processor-group membership protocol, dealing with a dynamically changing network of processors and reasoning in terms of local...
Coalgebraic specifications are used to formally describe the behaviour of classes in object-oriented languages. In this paper, a general notion of refinement between two such coalgebraic specifications is defined, capturing the idea that one “concrete” class specification realises the behaviour of the other, “abstract” class specification. Two (complete) proof-techniques are given to establish such refinements: one involving an invariant (a predicate that is closed under transitions) on the concrete class, and one involving a bisimulation (a relation that is closed under transitions) between the concrete and the abstract class. The latter can only be used if the abstract class is what we call totally specified. Parts of the underlying theory of invariants and bisimulations in a coalgebraic setting are included, involving least and greatest invariants and connections between invariants and bisimulations. Also, the proof-principles are illustrated in examples (which are fully formalised and verified in...
We introduce a necessary test for the claims about provable fault-tolerance: having proved to tolerate several faults, we must tolerate (provably) any combination of them. One notable failure to pass this test is bisimulation. The paper presents a class of bisimulations which are fault-monotonic and within CCS support compositional design of component specifications by stepwise refinement, each step...