Model checking Z specifications using SAL

Smith, Graeme and Wildman, Luke (2005). Model checking Z specifications using SAL. In: H. Treharne, S. King, M. Henson and S. Schneider, ZB 2005: Formal Specification and Development in Z and B. 4th Informational Conference of B and Z Users, Guildford, UK, (85-103). 13-15 April 2005. doi:10.1007/11415787_6

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Smith, Graeme
Wildman, Luke
Title of paper Model checking Z specifications using SAL
Conference name 4th Informational Conference of B and Z Users
Conference location Guildford, UK
Conference dates 13-15 April 2005
Proceedings title ZB 2005: Formal Specification and Development in Z and B   Check publisher's open access policy
Journal name Lecture Notes in Computer Science   Check publisher's open access policy
Place of Publication Berlin, Germany
Publisher Springer
Publication Year 2005
Sub-type Fully published paper
DOI 10.1007/11415787_6
ISBN 3540255591
ISSN 0302-9743
1611-3349
Editor H. Treharne
S. King
M. Henson
S. Schneider
Volume 3455
Start page 85
End page 103
Total pages 19
Collection year 2005
Language eng
Abstract/Summary The Symbolic Analysis Laboratory (SAL) is a suite of tools for analysis of state transition systems. Tools supported include a simulator and four temporal logic model checkers. The common input language to these tools was originally developed with translation from other languages, both programming and specification languages, in mind. It is, therefore, a rich language supporting a range of type definitions and expressions. In this paper, we investigate the translation of Z specifications into the SAL language as a means of providing model checking support for Z. This is facilitated by a library of SAL definitions encoding the Z mathematical toolkit.
Subjects E1
280302 Software Engineering
700199 Computer software and services not elsewhere classified
Keyword Z
Model checking
SAL
Tool support
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 17 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Thu, 23 Aug 2007, 20:59:43 EST