Formal Aspects of Computing

Items from 1 to 8 out of 8 results

article

Model checking action system refinements

Graeme Smith, Kirsten Winter

Formal Aspects of Computing > 2009 > 21 > 1-2 > 155-186

Action systems provide a formal approach to modelling parallel and reactive systems. They have a well established theory of refinement supported by simulation-based proof rules. This paper introduces an automatic approach for verifying action system refinements utilising standard CTL model checking. To do this, we encode each of the simulation conditions as a simulation machine, a Kripke structure...

article

Mutation testing in UTP

Bernhard K. Aichernig, He Jifeng

Formal Aspects of Computing > 2009 > 21 > 1-2 > 33-64

This paper presents a theory of testing that integrates into Hoare and He’s Unifying Theory of Programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory...

article

Graph transformations for object-oriented refinement

Liang Zhao, Xiaojian Liu, Zhiming Liu, Zongyan Qiu

Formal Aspects of Computing > 2009 > 21 > 1-2 > 103-131

An object-oriented program consists of a section of class declarations and a main method. The class declaration section represents the structure of an object-oriented program, that is the data, the classes and relations among them. The execution of the main method realizes the application by invoking methods of objects of the classes defined in the class declarations. Class declarations define the...

article

Relational concurrent refinement part II: Internal operations and outputs

Eerke Boiten, John Derrick, Gerhard Schellhorn

Formal Aspects of Computing > 2009 > 21 > 1-2 > 65-102

Two styles of description arise naturally in formal specification: state-based and behavioural. In state-based notations, a system is characterised by a collection of variables, and their values determine which actions may occur throughout a system history. Behavioural specifications describe the chronologies of actions—interactions between a system and its environment. The exact nature of such interactions...

article

A UTP semantics for Circus

Marcel Oliveira, Ana Cavalcanti, Jim Woodcock

Formal Aspects of Computing > 2009 > 21 > 1-2 > 3-32

Circus specifications define both data and behavioural aspects of systems using a combination of Z and CSP constructs. Previously, a denotational semantics has been given to Circus; however, a shallow embedding of Circus in Z, in which the mapping from Circus constructs to their semantic representation as a Z specification, with yet another language being used as a meta-language, was not useful for...

article

Editorial

Eerke Boiten

Formal Aspects of Computing > 2009 > 21 > 1-2 > 1-1

article

Trace-based derivation of a scalable lock-free stack algorithm

Lindsay Groves, Robert Colvin

Formal Aspects of Computing > 2009 > 21 > 1-2 > 187-223

We show how a sophisticated, lock-free concurrent stack implementation can be derived from an abstract specification in a series of verifiable steps. The algorithm is based on the scalable stack algorithm of Hendler et al. (Proceedings of the sixteenth annual ACM symposium on parallel algorithms, 27–30 June 2004, Barcelona, Spain, pp 206–215), which allows push and pop operations to be paired off...

article

FDR Explorer

Leo Freitas, Jim Woodcock

Formal Aspects of Computing > 2009 > 21 > 1-2 > 133-154

We describe: (1) the internal structures of FDR, the refinement model checker for Hoare’s Communicating Sequential Processes (CSP); and (2) an application-programming interface (API) that allows users to interact more closely with FDR and to have finer-grain control over its behaviour and data structures. This API makes it possible to create optimised CSP code to perform refinement checks that are...

Filter options

Number:
1-2
Volume:
21
Year:
2009

Publication date

Set your own date range

Keywords

MODEL CHECKING (2)
REFINEMENT (2)
REFINEMENT CALCULUS (2)
ACTION SYSTEMS (1)
ALGEBRA OF PROGRAMMING (1)
AUTOMATA (1)
CLASS GRAPH (1)
CONCURRENCY (1)
CSP (1)
CTL (1)
DATA REFINEMENT (1)
DEADLOCK (1)
FAILURES–DIVERGENCES REFINEMENT (1)
FAULT-BASED TESTING (1)
FDR (1)
GRAPH TRANSFORMATION (1)
INTERNAL OPERATIONS (1)
KIV (1)
LABELLED TRANSITION SYSTEMS (1)
MECHANISATION (1)
MUTATION TESTING (1)
NORMAL FORM (1)
OBJECT GRAPH (1)
OBJECT-ORIENTATION (1)
OUTPUTS (1)
RELATIONAL MODEL (1)
SIMULATIONS, PROCESS ALGEBRAIC SEMANTICS (1)
SPECIFICATION-BASED TESTING (1)
STRUCTURE REFINEMENT (1)
THEOREM PROVING (1)
UNIFYING THEORIES OF PROGRAMMING (1)
Z (1)
more

INFONA - science communication portal

Formal Aspects of Computing

Add recipient

Sending message cancelled

Are you sure you want to cancel sending this message?

Send message

Filter options

Publication date

Date range setting

Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.

Keywords

Reporting an error / abuse

Sending the report failed

Accessibility options