Challenging Formal Specifications by Mutation: a CSP security example

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Thitima Srivatanakul Articles by John A. Clark Articles by Susan Stepney Articles by Fiona Polack

10th Asia-Pacific Software Engineering Conference (APSEC'03)

Chiang Mai, Thailand

December 10-December 12

ISBN: 0-7695-2011-1

	ASCII Text	x
	Thitima Srivatanakul, John A. Clark, Susan Stepney, Fiona Polack, "Challenging Formal Specifications by Mutation: a CSP security example," Asia-Pacific Software Engineering Conference, pp. 340, 10th Asia-Pacific Software Engineering Conference (APSEC'03), 2003.

	BibTex	x
	@article{ 10.1109/APSEC.2003.1254388, author = {Thitima Srivatanakul and John A. Clark and Susan Stepney and Fiona Polack}, title = {Challenging Formal Specifications by Mutation: a CSP security example}, journal ={Asia-Pacific Software Engineering Conference}, volume = {0}, year = {2003}, isbn = {0-7695-2011-1}, pages = {340}, doi = {http://doi.ieeecomputersociety.org/10.1109/APSEC.2003.1254388}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Asia-Pacific Software Engineering Conference TI - Challenging Formal Specifications by Mutation: a CSP security example SN - 0-7695-2011-1 SP EP A1 - Thitima Srivatanakul, A1 - John A. Clark, A1 - Susan Stepney, A1 - Fiona Polack, PY - 2003 KW - CSP KW - model checking KW - mutation testing KW - security properties VL - 0 JA - Asia-Pacific Software Engineering Conference ER -

Thitima Srivatanakul, University of York, Heslington

John A. Clark, University of York, Heslington

Susan Stepney, University of York, Heslington

Fiona Polack, University of York, Heslington

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/APSEC.2003.1254388

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.

Index Terms:

CSP, model checking, mutation testing, security properties

Citation:

Thitima Srivatanakul, John A. Clark, Susan Stepney, Fiona Polack, "Challenging Formal Specifications by Mutation: a CSP security example," apsec, pp.340, 10th Asia-Pacific Software Engineering Conference (APSEC'03), 2003

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.