You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: University of York » Outputs » Detail

Output details

11 - Computer Science and Informatics

University of York

Return to search Previous output Next output

Output 123 of 139 in the submission

Article title

Testing for refinement in Circus

Type

D - Journal article

DOI

10.1007/s00236-011-0133-z

Title of journal

Acta Informatica

Article number

Volume number

Issue number

First page of article

ISSN of journal

0001-5903

Year of publication

2011

URL

http://link.springer.com/article/10.1007%2Fs00236-011-0133-z

Number of additional authors

Additional information

<07>Originality: Back in the 90's, Gaudel published a seminal paper, "Testing can be formal too", and created a new area of research: formal testing. This is the first instantiation of Gaudel's theory in which all proofs are formal. Rigour: Results proved using Hoare’s and He’s unifying theories of programming. Significance: Foundation for sound testing techniques for refinement using state-rich process algebra. Circus, in particular, is used to verify software in aerospace applications and novel virtualisation software by the US Naval Research Laboratory. Work led to further funding from the Royal Society and CNRS, and new collaborations with Brunel and Brazil.

Interdisciplinary

Cross-referral requested

Research group

A - High Integrity Systems Engineering

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract