Skip to main content
main-content

Inhaltsverzeichnis

Frontmatter

Specification Coverage for Testing in Circus

The Unifying Theories of Programming underpins the development of

Circus

, a state-rich process algebra for refinement. We have previously presented a theory of testing for

Circus

; it gives a symbolic characterisation of tests. Each symbolic test specifies constraints that capture the effect of the possibly nondeterministic state operations, and their interaction. This is a sound basis for testing techniques based on constraint solving for generation of concrete tests, but does not support well selection criteria based on the structure of the specification. We present here a labelled transition system that captures information about a

Circus

model and its structure. It is useful for testing techniques based on specification coverage. The soundness argument for the new transition system follows the UTP style, but relates the new transition relation to the

Circus

relational model and its operational semantics.

Ana Cavalcanti, Marie-Claude Gaudel

UTP and Sustainability

Hoare and He’s approach to unifying theories of programming, UTP, is a dozen years old. In spite of the importance of its ideas, UTP does not seem to be attracting due interest. The purpose of this article is to discuss why that is the case, and to consider UTP’s destiny. To do so it analyses the nature of UTP, focusing primarily on unification, and makes suggestions to expand its use.

Yifeng Chen, Jeff W. Sanders

A Probabilistic BPEL-Like Language

Exception and failure are the typical phenomena of the execution of long-running transactions. To capture the random features of internet-based computing, this paper investigates a BPEL-like language which is enriched with probabilistic choice operator. We extend the standard design model [12] with the new healthiness conditions to accommodate the coordination and compensation mechanisms of the language.

He Jifeng

On Modelling User Observations in the UTP

This paper presents an approach for modelling interactions between users and systems in the

Unifying Theories of Programming

. Working in the predicate calculus, we outline generic techniques for calculating a user’s observations of a system and, in turn, for identifying the information that a user can deduce about the system’s behaviour from those observations. To demonstrate how this approach can be applied in practical software development, we propose some alternative refinement relations that offer greater flexibility than classical refinement by utilising knowledge of the observational abilities of users.

Michael J. Banks, Jeremy L. Jacob

Unifying Theories of Confidentiality

This paper presents a framework for reasoning about the security of confidential data within software systems. A novelty is that we use Hoare and He’s

Unifying Theories of Programming

(UTP) to do so and derive advantage from this choice. We identify how information flow between users can be modelled in the UTP and devise conditions for verifying that system designs may not leak secret information to untrusted users. We also investigate how these conditions can be combined with existing notions of refinement to produce refinement relations suitable for deriving secure implementations of systems.

Michael J. Banks, Jeremy L. Jacob

Saoithín: A Theorem Prover for UTP

Saoithín

is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higher-order logic, alphabets, equational reasoning and “programs as predicates” style that is prevalent in much of the UTP literature, from the seminal work by Hoare & He [HH98] onwards. This paper describes the key features of the theorem prover, with an emphasis on the underlying foundations, and how these affect the design and implementation choices. These key features include: a formalisation of a UTP Theory; support for common proof strategies; sophisticated goal/law matching ; and user-defined language constructs. A simple theory of designs with some proof extracts is used to illustrate the above features. The theorem prover has been used with undergraduate students and we discuss some of those experiences. The paper then concludes with a discussion of current limitations and planned improvements to the tool.

Andrew Butterfield

A Formal Approach to Analyzing Interference Problems in Aspect-Oriented Designs

Interference problems in aspect-oriented designs refer to the undesired interference between aspects and base programs that can lead to the emergence of unexpected behaviors, which do harm to the correctness of the entire system. We present a rigorous approach to analyzing the interference problems in aspect-oriented designs. Formal representations of classes and aspects are defined in terms of

designs

in UTP, while the weaving techniques in AOP are interpreted as the compositions of corresponding formal models. Conflicts between an aspect and base programs as well as between two aspects can be detected by calculating the weakest preconditions. Furthermore, the calculation also provides informative guidelines on how to solve the conflicts it found. Early detecting and removing conflicts in aspect-oriented design models can improve their qualities and save plenty of costs.

Xin Chen, Nan Ye, Wenxu Ding

Programmable Verifiers in Imperative Programming

This paper studies the relation between execution and verification. A simple imperative language called VerExec with execution and verification commands is introduced. A machine only executes execution commands of a program, while the compiler only performs the verification commands. Common commands in other languages can be defined as a combination of execution and verification commands. Design of verifiers then becomes program design using verification commands. It is shown that type checking, abstract interpretation, modeling checking and Hoare Logic are all special verification programs, so are many of their combinations.

Yifeng Chen

Unifying Theories in Isabelle/HOL

In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL.

Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and

Circus

. The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation.

Abderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff

Unifying Recursion in Partial, Total and General Correctness

We give an algebraic semantics of non-deterministic, sequential programs which is valid for partial, total and general correctness. It covers full recursion based on a unified approximation order. We provide explicit solutions in terms of the refinement order. As an application, we systematically derive a semantics of while-programs common to the three correctness approaches.

UTP’s designs and prescriptions represent programs as pairs of termination and state transition information in total and general correctness, respectively. We show that our unified semantics induces a pair-based representation which is common to the correctness approaches. Operations on the pairs, including finite and infinite iteration, can be derived systematically. We also provide the effect of full recursion on the unified, pair-based representation.

Walter Guttmann

Halting Still Standing – Programs versus Specifications

In UTP’06 [4], Hehner claims that the traditional proof of the incomputability of the Halting Function is rather a proof of the inconsistency of its specification. We identify where his argument fails.

Hehner claims that assuming a well-defined Halting Function for specifications leads to a contradiction by a very similar argument as assuming a computable Halting Function for programs does. In the case of programs, this argument leads to concluding that the Halting Function is not computable, porting the proof to the case of specifications, it is claimed to allow concluding that the Halting Function is ill-defined. He reasons that if the Halting Function for specifications is ill-defined, then the concept of the Halting Function in general is inconsistent, including the one for programs. We do not challenge this generalization, but rather point out a flaw in his argument for the specification case. We formalize his argument in UTP-style. This enables us to show that there is a subtle tacit assumption being made about the recursive definition that is used to arrive at the contradiction, namely that the defining equation has a solution. We also explain why this does not affect the proof for the program case. Furthermore, we analyze whether recursion in the language Hehner uses is essential for his argument and our refutation. Porting the arguments to a language without recursion shows that the issue of the existence of the contradicting specification remains. We conclude that this line of argument does not challenge the healthiness of the concept of the Halting Function, including its extension to specifications.

Cornelis Huizing, Ruurd Kuiper, Tom Verhoeff

Promoting Models

There can be multitudinous models specifying aspects of the same system. Each model has a bias towards one aspect. These models often override in specific aspects though they have different expressions. A specification written in one model can be refined by introducing additional information from other models. The paper proposes a concept of promoting models which is a methodology to obtain refinements with support from cooperating models. It refines a primary model by integrating the information from a secondary model. The promotion principle is not merely an academic point, but also a reliable and robust engineering technique which can be used to develop software and hardware systems. It can also check the consistency between two specifications from different models. A case of modeling a simple online shopping system with the cooperation of the guarded design model and CSP model illustrates the practicability of the promotion principle.

Qin Li, Yongxin Zhao, Xiaofeng Wu, Si Liu

Probabilistic Choice, Reversibility, Loops, and Miracles

We consider an addition of probabilistic choice to Abrial’s Generalised Substitution Language (GSL) in a form that accommodates the backtracking interpretation of non-deterministic choice. Our formulation is introduced as an extension of the Prospective Values formalism we have developed to describe the results from a backtracking search. Significant features are that probabilistic choice is governed by feasibility, and non-termination is strict. The former property allows us to use probabilistic choice to generate search heuristics. In this paper we are particularly interested in iteration. By demonstrating sub-conjunctivity and monotonicity properties of expectations we give the basis for a fixed point semantics of iterative constructs, and we consider the practical proof treatment of probabilistic loops. We discuss loop invariants, loops with probabilistic behaviour, and probabilistic termination in the context of a formalism in which a small probability of non-termination can dominate our calculations, proposing a method of limits to avoid this problem. The formal programming constructs described have been implemented in a reversible virtual machine (RVM).

Bill Stoddart, Pete Bell

Towards a Pomset Semantics for a Shared-Variable Parallel Language

In this paper we present a pomset semantics for a shared-variable parallel language which is an extension of the one studied by Brookes in [5]. The pomset semantics lifts the transition trace semantics to the non-interleaving setting, where parallel events in a pomset transition trace are labeled by

conditionally independent

actions. Most of the important laws from the interleaving setting also hold in the non-interleaving setting. Similarities and differences with other related works are discussed.

Yongxin Zhao, Xu Wang, Huibiao Zhu

Generating Denotational Semantics from Algebraic Semantics for Event-Driven System-Level Language

As a system-level modelling language, SystemC possesses several novel features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. We have explored the denotational semantics [15] for SystemC using

Unifying Theories of Programming

(abbreviated as UTP) [6], where algebraic laws can be achieved based on the denotational model.

In this paper, we consider the inverse work; i.e., generating the denotational semantics from algebraic semantics for SystemC. A complete set of algebraic laws is explored.The concept of head normal from is applied in supporting the calculation. We also explore the simulation of algebraic laws and head normal form. Based on this, the mechanical derivation of denotational semantics from algebraic semantics is also studied.

Huibiao Zhu, Fan Yang, Jifeng He

Backmatter

Weitere Informationen

Premium Partner

Neuer Inhalt

BranchenIndex Online

Die B2B-Firmensuche für Industrie und Wirtschaft: Kostenfrei in Firmenprofilen nach Lieferanten, Herstellern, Dienstleistern und Händlern recherchieren.

Whitepaper

- ANZEIGE -

Best Practices für die Mitarbeiter-Partizipation in der Produktentwicklung

Unternehmen haben das Innovationspotenzial der eigenen Mitarbeiter auch außerhalb der F&E-Abteilung erkannt. Viele Initiativen zur Partizipation scheitern in der Praxis jedoch häufig. Lesen Sie hier  - basierend auf einer qualitativ-explorativen Expertenstudie - mehr über die wesentlichen Problemfelder der mitarbeiterzentrierten Produktentwicklung und profitieren Sie von konkreten Handlungsempfehlungen aus der Praxis.
Jetzt gratis downloaden!

Bildnachweise