An Instance to Extend Object-Z Formal Specification

Xiao Mao Hou; Ling Ma; Zhi Cheng Wen

doi:10.4028/www.scientific.net/AMR.846-847.1500

Paper Titles

Research on the Service Navigation System of Engineering Machinery Industry Integration Platform Based on Cloud Computing
p.1483

WiFi Wireless Video Transmission Technology's Application in Intelligent Home
p.1487

Model Design of Self-Service Intelligent Resource Management System Based on Cloud Platform
p.1491

Research on the Visual Communication Design Based on Digital Multimedia
p.1496

An Instance to Extend Object-Z Formal Specification
p.1500

Modeling and Simulation of Standard II Missiles Intercepting a Low Target
p.1505

New Technologies of Electronic Toll Collection Based on Cloud Computing
p.1509

Video Tracker Integrated Test System Design
p.1514

RFID Mutual Authentication Protocol Based on Chaos Key
p.1519

HomeAdvanced Materials ResearchAdvanced Materials Research Vols. 846-847An Instance to Extend Object-Z Formal...

An Instance to Extend Object-Z Formal Specification

Abstract:

Object-Z, an extension to formal specification language Z, is good for describing large scale Object-Oriented software specification. This paper introduces Real-Time Object-Z and describes the characters of real-time system: delay, timeout and multithread. Real-Time Object-Z consists two parts: functional specification and filter specification. While Object-Z has found application in a number of areas, its utility is limited by its inability to specify continuous variables and real-time constraints. The main benefit is that it is convenient to deal with the timing variables defined in the specification developed with our approach. The effective specification after applying filter part to functional part holds the form of specification developed with Object-Z. Expanded Object-Z, a modular formal specification language, is a minimum extension of the syntax and semantics of Object-Z. The main advantage of this extension lies in that it is convenient to describe and verify the complex real-time software specification.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Advanced Materials Research (Volumes 846-847)

Pages:

1500-1504

DOI:

https://doi.org/10.4028/www.scientific.net/AMR.846-847.1500

Citation:

Cite this paper

Online since:

November 2013

Authors:

Xiao Mao Hou*, Ling Ma, Zhi Cheng Wen

Keywords:

Formal Specification, Object-Z, Real-Time

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

* - Corresponding Author

References

[1] Brendan Mahony, Jin Song Dong, Blending Object-Z and Timed CSP: An introduction to TCOZ, ICSE, 1998, pp: 95-104.

DOI: 10.1109/icse.1998.671106

Google Scholar

[2] Jing Sun, Jing Song Dong, Specifying and Reasoning about Generic Architecture in TCOZ, APSEC, 2002, pp: 405-419.

DOI: 10.1109/apsec.2002.1183010

Google Scholar

[3] Mahony, B. P. and Dong, J. S, Timed Communicating Object Z, IEEE Transactions on Software Engineering, 2000, pp: 150-177.

DOI: 10.1109/32.841115

Google Scholar

[4] Smith, G. and Ian Hayes, Structuring Real-Time Object-Z specifications, Springer-Verlag IFM, 2000, pp: 97-115.

Google Scholar

[5] Smith, G, The Object-Z Specification Language, Advances in Formal Methods, Kluwer Academic Publishers, (1999).

Google Scholar

[6] K. Periyyasamy, V. S. Alagar, Adding Real-Time Filters to Object- Oriented Specification of Time critical Systems, ISFST, 1998, pp: 28-40.

DOI: 10.1109/wift.1998.766295

Google Scholar

[7] M. Aksit et al, Real-time specification inheritance anomalies and real-time filters, In ECOOP'94, Springer-Verlag, pp: 386-407.

DOI: 10.1007/bfb0052193

Google Scholar

[8] Graeme Smith, Reasoning about Object-Z specification, APSEC 1995, Page(s): 489–497.

Google Scholar