This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Formal Framework for ASTRAL Intralevel Proof Obligations
August 1994 (vol. 20 no. 8)
pp. 548-561

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL specifications. ASTRAL is provided with structuring mechanisms that allow one to build modularized specifications of complex systems with layering. In this paper, further details of the ASTRAL environment components and the critical requirements components, which were not fully developed in previous papers, are presented. Formal proofs in ASTRAL can be divided into two categories: interlevel proofs and intralevel proofs. The former deal with proving that the specification of level i+1 is consistent with the specification of level i, and the latter deal with proving that the specification of level i is consistent and satisfies the stated critical requirements. This paper concentrates on intralevel proofs.

[1] R. Alur, C. Courcoubetis, and D. Dill, "Model-checking for real-time systems," inProc. 5th Annual IEEE Symp. Logic in Computer Science, pp. 414-425, 1990.
[2] C. Chang, H. Huang, and C. C. Song, "An approach to verifying concurrency behavior of real-time systems based on time Petri net and temporal logic,"InfoJapan 90, 1990, pp. 307-314.
[3] A. Coen-Porisini, R. Kemmerer, and D. Mandrioli, "Formal verification of real-time systems in ASTRAL," Tech. Rep. TRCS 92-22, Dept. of Comput. Sci., Univ. of California, Santa Barbara, CA, USA, Sept. 1992.
[4] A. Coen-Porisini, R. Kemmerer, and D. Mandrioli, "A formal framework for ASTRAL interlevel proof obligations," Tech. Rep. TRCS 93-04, Dept. of Comput. Sci., Univ. of California, Santa Barbara, CA, USA, Apr. 1993.
[5] M. Felder, D. Mandrioli, and A. Morzenti, "Proving properties of real-time systems through logical specifications and Petri net models,"IEEE Trans. Software Eng., vol. 20, pp. 127-141, Feb. 1994.
[6] A. Gabrielian and M. Franklin,"Multilevel specification of real-time systems,"Comm. of ACM 34, pp. 51-60, May 1991.
[7] R. Gerber and I. Lee, "A layered approach to automating the verification of real-time system,"IEEE Trans. Software Eng., vol. 18, pp. 768-784, Sept. 1992.
[8] C. Ghezzi and R. Kemmerer, "ASTRAL: An assertion language for specifying real-time systems," inProc. 3rd European Software Engineering Conf., Milan, Italy, pp. 122-146, Oct. 1991.
[9] C. Ghezzi and R. Kemmerer, "Executing formal specifications: The ASTRAL to TRIO translation approach," inProc. TAV4: Symp. Testing, Anal., Verification, 1991, pp. 112-119.
[10] J. Ostroff,Temporal Logic of Real-Time Systems. Research Studies Press, 1990.
[11] A. Pnueli, "The temporal logic of programs," inProc. 18th Annu. Symp. Foundations of Comput. Sci., 1977, pp. 46-57.
[12] I. Suzuki, "Formal analysis of alternating bit protocol by temporal Petri nets,"IEEE Trans. Software Eng.vol. 16, pp. 1273-1281, Nov. 1990.
[13] P. Zave, "PAISLey user documentation volume 3: Case studies," Comput. Technol. Res. Lab. Rep., AT&T Bell Laboratories, Murray Hill, NJ, USA, 1987.

Index Terms:
formal specification; real-time systems; finite state machines; program verification; specification languages; intralevel proof obligations; ASTRAL; formal specification language; real-time systems; formal software development; mathematical correctness; formal methods; formal specification; verification; timing requirements; formal proof; state machines; ASLAN; TRIO
Citation:
A. Coen-Porisini, R.A. Kemmerer, D. Mandrioli, "A Formal Framework for ASTRAL Intralevel Proof Obligations," IEEE Transactions on Software Engineering, vol. 20, no. 8, pp. 548-561, Aug. 1994, doi:10.1109/32.310665
Usage of this product signifies your acceptance of the Terms of Use.