home > publications > CSP, occam, Handel-C > Challenging formal specifications by mutation...

Thitima Srivatanakul, John A. Clark, Susan Stepney, Fiona Polack.
Challenging formal specifications by mutation: a CSP security example.

APSEC-2003: 10th Asia-Pacific Software Engineering Conference, Chiang Mai, Thailand, December, 2003 , pp 340-350. IEEE, 2003

Abstract:

When formal modelling is done we must validate both the model and the assumptions. Formal techniques tend to concentrate on the former. We examine how fault injection (specification mutation) and model checking can help address the latter, in particular, the effects of failure. We find that, in contrast with software testing, where they are a problem, "equivalent mutants" are valuable for specification validation.

full paper : Postscript 169K | RefineNet talk : PDF 280K 

@inproceedings(SS-APSEC03,
  author = "Thitima Srivatanakul and John A. Clark
            and Susan Stepney and Fiona Polack",
  title = "Challenging formal specifications by mutation:
           a {CSP} security example",
  pages = "340--350",
  crossref = "APSEC03"
)

@proceedings(APSEC03,
  title = "APSEC-2003: 10th Asia-Pacific Software Engineering Conference,
           Chiang Mai, Thailand, December 2003",
  booktitle = "APSEC-2003: 10th Asia-Pacific Software Engineering Conference,
               Chiang Mai, Thailand, December 2003",

  publisher = "IEEE",
  year = 2003
)