bullet Sensors & Transducers Journal

    (ISSN 1726- 5479)

205.767

2008 e-Impact Factor

25 Top Downloaded Articles

Best Selling Articles 2012

Journal Subscription 2013

Editorial Calendar 2013

Submit an Article

Editorial Board

Current Issue

S&T journal's cover

Sensors & Transducers Journal 2011

Sensors & Transducers Journal 2010

Sensors & Transducers Journal 2009

Sensors & Transducers Journal 2008

Sensors & Transducers Journal 2007

2000-2002 S&T e-Digest Contents

2003 S&T e-Digest Contents

2004 S&T e-Digest Contents

2005 S&T e-Digest Contents

2006 S&T e-Digest Contents

 

Best Articles 2011

 

 

 

Vol. 154, Issue 7, July 2013, pp. 266-273

 

Bullet

 

Model Checking Object-Z Specification Using SPIN
 
1 Lei Xiao, 2 Gongzheng Lu, 1 Shunzhi Zhu

1 School of Computer and Information Engineering of Xiamen University of Technology, Xiamen, 361024, China

2 Department of Computer Engineering, Suzhou Vacational University, Suzhou, 215000, China
Tel.: 15960810542, fax: 0086-0592-6291390
E-mail: lxiao@xmut.edu.cn

 

Received: 2 May 2013   /Accepted: 19 July 2013   /Published: 31 July 2013

Digital Sensors and Sensor Sysstems

 

Abstract: Nowadays, model checking is recognized as an efficient technology for verifying system properties. There are many tools such as SPIN and NuSMV supports model checking that will greatly enhance software systems applicability. However, it is difficult to establish a tool to directly verify Object-Z, because of its high-level abstraction. This paper puts the Object-Z specification into label transition system (LTS), and then translates the LTS into the input language Promela of Spin. Subsequently, the history invariant in Object-Z is described by Linear Temporal Logic (LTL). So the correctness of Object-Z specification can be verified.

 

Keywords: Model checking, Object-Z, LTS, SPIN, LTL.

 

Acrobat reader logo Click <here> or title of paper to download the full pages article in pdf format

 

 

Download <here> the Library Journal Recommendation Form

 

 

 

 

 


1999 - 2018 Copyright , International Frequency Sensor Association (IFSA). All Rights Reserved.


Home - News - Links - Archives - Tools - Voltage-to-Frequency Converters - Standardization - Patents - Marketplace - Projects - Wish List - e-Shop - Sensor Jobs - Membership - Videos - Publishing - Site Map - Subscribe - Search

 Members Area -Sensors Portal -Training Courses - S&T Digest - For advertisers - Bookstore - Forums - Polls - Submit Press Release - Submit White Paper - Testimonies - Twitter - Facebook - LinkedIn