Extending Object-Z Formal Specification with Real-Time

Zhi Cheng Wen; Zhi Gang Chen

doi:10.4028/www.scientific.net/AMM.263-266.1642

Paper Titles

Design and Implementation of ARM-Based Mobile Handheld Terminal for Community Medical
p.1623

Design of Virtual Machine Monitor for Embedded Systems
p.1629

Determination of Parting Lines and Multiple-Undercut Boundaries for Complex CAD Parts with Application to Multi-Piece Molds Design
p.1633

Exploration and Practice in MCU Course Teaching Based on CDIO Mode
p.1638

Extending Object-Z Formal Specification with Real-Time
p.1642

Fault Diagnosis System of A²/O Process Based on Parameter Estimation and Expert System
p.1647

Intelligent Match of Emergency Plan Based on Chinese Keywords Extraction
p.1652

Mechanism and Implementation of Distributed Workflow for Electric Power Dispatching
p.1659

Mobile Cache of CGML Spatial Data
p.1664

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 263-266Extending Object-Z Formal Specification with...

Extending Object-Z Formal Specification with Real-Time

Abstract:

This paper extends Object-Z with Real-Time and describes the characters of real-time system: delay, timeout and multithread. Real-Time Object-Z consists two parts: functional specification and filter specification. The both for any time critical system can be developed with two parts. Functional specification developed with Object-Z formerly can be reused. The main benefit is that it is convenient to deal with the timing variables defined in the specification developed with our approach. Using our approach, we can develop real-time specification and reason about the real-time properties conveniently.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 263-266)

Pages:

1642-1646

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.263-266.1642

Citation:

Cite this paper

Online since:

December 2012

Authors:

Zhi Cheng Wen, Zhi Gang Chen

Keywords:

Filter Specification, Object-Z, Real-Time

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

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