This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Specification of Realtime Systems Using ASTRAL
September 1997 (vol. 23 no. 9)
pp. 572-598

Abstract—ASTRAL is a formal specification language for realtime systems. It is intended to support formal software development and, therefore, has been formally defined. The structuring mechanisms in ASTRAL allow one to build modularized specifications of complex systems with layering. A realtime system is modeled by a collection of state machine specifications and a single global specification. This paper discusses the rationale of ASTRAL's design. ASTRAL's specification style is illustrated by discussing a telephony example. Composability of one or more ASTRAL system specifications is also discussed by the introduction of a composition section, which provides the needed information to combine two or more ASTRAL system specifications.

[1] R. Alur, C. Courcoubetis, and D. Dill, “Model-Checking for Real-Time Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[2] R. Alur and D.L. Dill,“The theory of timed automata,” Real-Time: Theory in Practice, J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rosenberg, eds., Lecture Notes in Computer Science #600, pp. 28-73. Springer-Verlag, 1991.
[3] R. Alur, T. Feder, and T. Henzinger, "The Benefits of Relaxing Punctuality," Proc. 10th ACM Symp. Principles of Distributed Computing, pp. 139-152, 1991.
[4] B. Auernheimer and R.A. Kemmerer, "ASLAN User's Manual," TRCS84-10, Dept. of Computer Science, Univ. of California, Santa Barbara, Apr. 1992.
[5] B. Auernheimer and R.A. Kemmerer, "Procedural and Nonprocedural Semantics of the ASLAN Formal Specification Language," Proc. 19th Ann. Hawaii Int'l Conf. System Sciences,Honolulu, Hawaii, Jan. 1986.
[6] B. Auernheimer and R.A. Kemmerer, “Rt-aslan: A Specification Language for Real-Time Systems,” IEEE Trans. Software Eng., vol. 12, no. 9, Sept. 1986.
[7] M. Abadi and L. Lamport, “An Old-Fashioned Recipe for Real Time,” Proc. REX Workshop, Real-Time Theory in Practice, pp. 1-27, June 1991.
[8] M. Abadi and L. Lamport, "Conjoining Specifications," ACM Trans. Programming Languages and Systems, Vol. 17, No. 3, May 1995, pp. 507-534.
[9] K. Brink, L. Bun, J. van Katwijk, and W.J. Toetenel, "Hybrid Specification of Control Systems," First IEEE Int'l Conf. Eng. Complex Computer Systems,Ft. Lauderdale, Fla., Nov. 1995.
[10] G. Buonanno, A. Coen-Porisini, and W. Fornaciari, "Hardware Specification Using the Assertion Language ASTRAL," Proc. Advanced Research Workshop Correct Hardware Design Methodologies,Torino, Italy, June 1991.
[11] H.E. Bal, J.G. Steiner, and A.S. Tanenbaum, "Programming Languages for Distributed Computing Systems," ACM Computing Surveys, Vol. 21, No. 3, Sept. 1989, pp. 261-322.
[12] F. Boussinot and R. de Simone, "The Esterel Language," Another Look at Real Time Programming, Proc. IEEE, vol. 79, pp. 1,293-1,304, 1991.
[13] K.M. Chandy and J. Misra, Parallel Program Design—A Foundation. Addison-Wesley, 1988.
[14] A. Coen-Porisini and R.A. Kemmerer, "The Composability of ASTRAL Realtime Specifications," Proc. Int'l Symp. Software Testing and Analysis,Cambridge, Mass., July 1993.
[15] A. Coen-Porisini, R. Kemmerer, and D. Mandrioli, “A Formal Framework for ASTRAL Intra Level Proof Obligations,” IEEE Trans. Software Eng., vol. 20, no. 8, pp. 548-561, Aug. 1994.
[16] A. Coen-Porisini, R.A. Kemmerer, and D. Mandrioli, "A Formal Framework for ASTRAL Inter-level Proof Obligations," Proc. Fifth European Software Eng. Conf.,Barcelona, Spain, Sept. 1995.
[17] A. Coen-Porisini, P. San Pietro, and R. Kemmerer, "Formal Semantics Definition for ASTRAL," Report No. TRCS 94-15, Dept. of Computer Science, Univ. of California, Santa Barbara, Sept. 1994.
[18] B. Dasarathy, "Timing Constraints of Real-Time Systems: Constructs for Expressing Them, Methods for Validating Them," IEEE Trans. Software Eng., vol. 11, no. 1, Jan. 1985.
[19] L.K. Dillon, G.S. Avrunin, and J.C. Wileden, "Constrained Expressions: Toward Broad Applicability of Analysis Methods for Distributed Software Systems," ACM Trans. Programming Languages and Systems, vol. 10, no. 3, pp. 374-402, July 1988.
[20] J. Douglas and R.A. Kemmerer, "Aslantest: A Symbolic Execution Tool for Testing ASLAN Formal Specifications," Proc. ISTSTA '94—Int'l Symp. Software Testing and Analysis, ACM Software Engineering Notes, pp. 15-27, 1994.
[21] G. De Pietro and U. Villano, "A Clock Synchronization Algorithm for the Performance Analysis of Multicomputer Systems," Concurrency: Practice and Experience, vol. 6, no. 8, pp. 653-671, Dec. 1994.
[22] S.R. Faulk and D.L. Parnas, On Synchronization in Hard-Real-Time Systems Comm. ACM, vol. 31, pp. 274-287, Mar. 1988.
[23] M. Felder and A. Morzenti, “Validating Real-Time Systems by History-Checking TRIO Specifications,” ACM Trans. Software Eng. and Methodologies, vol. 3, no. 4, Oct. 1994.
[24] 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, no. 2, pp. 127–141, Feb. 1994.
[25] A. Gabrielian and M. Franklin, "Multilevel Specification of Realtime Systems," Comm. ACM, vol. 34, no. 5, pp. 51-60, May 1991.
[26] P. Le Guernic, T. Gautier, M. Le Borgne, and C. Le Maire, "Programming Real-Time Applications with SIGNAL," Proc. IEEE, vol. 79, no. 9, Sept. 1991.
[27] C. Ghezzi and R.A. Kemmerer, "ASTRAL: An Assertion Language for Specifying Realtime Systems," Proc. Third European Software Eng. Conf.,Milano, Italy, Oct. 1991.
[28] C. Ghezzi and R.A. Kemmerer, "Executing Formal Specifications: The ASTRAL to TRIO Translation Approach," Proc. Symp. Testing, Analysis, and Verification,Victoria, B.C., Canada, Oct. 1991.
[29] R. Gerber and I. Lee, "A Layered Approach to Automating the Verification of Real-Time Systems," IEEE Trans. Software Eng., vol. 18, no. 9, pp. 768-784, Sept. 1992.
[30] C. Ghezzi et al., "A General Way to Put Time in Petri Nets," Proc. Fourth Int'l Workshop Software Design and Specification,Monterey, Calif., Apr. 1987.
[31] C. Ghezzi, D. Mandriolli, and A. Morzenti, "Trio: A Logic Language for Executable Specifications of Real-Time Systems," J. Systems and Software, vol. 12, no. 2, pp. 107-123, May 1990.
[32] H. Gomaa, "Software Design Methods for the Design of Large-Scale Real-Time Systems," J. Systems and Software, vol. 25, no. 2, pp. 127-146, May 1994.
[33] D. Harel, “Statecharts: A Visual Approach to Complex Systems,” Science of Computer Programming, Vol. 8, No. 3, pp. 231–274, 1987.
[34] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, "The Synchronous Data-Flow Programming Language LUSTRE," Proc. IEEE, vol. 79, no. 9, pp. 1,305-1,320, Sept. 1991.
[35] C. Heitmeyer and N. Lynch, "The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems," Proc. Real-Time Systems,San Juan, Puerto Rico, Dec. 1994.
[36] D. Harel,H. Lachover,A. Naamad,A. Pnueli,M. Politi,R. Sherman,A. Shtul-Trauring,“Statemate: A working environment for the development of complex reactive systems,” Proc. 10th Int’l Conf. Software Eng. (ICSE 10), IEEE Computer Soc., pp. 396-406, 1988.
[37] C. Ratel, N. Halbwachs, and P. Raymond, "Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE," IEEE Trans. Software Eng., vol. 18, no. 9, pp. 785-793, Sept. 1992.
[38] D.J. Hatley and I.A. Pirbhai,Strategies for Real-Time System Specification, Dorset House, 1987.
[39] M.S. Jaffe and N.G. Leveson, "Completeness, Robustness, and Safety in Real-Time Software Requirements Specification," Proc. 11th Int'l Conf. Software Eng.,Pittsburgh, Penn., May 1989.
[40] F. Jahanian and A. K.-L. Mok,“Safety analysis of timing properties in real-time systems,”IEEE Trans. Software Eng., vol. SE-12, pp. 890–904, Sept. 1986.
[41] F. Jahanian and A.K. Mok, "Modechart: A Specification Language for Real-Time Systems," IEEE Trans. Software Eng., vol. 20, no. 10, pp. 879-889, Oct. 1994.
[42] R.A. Kemmerer, "Testing Software Specifications to Detect Design Errors," IEEE Trans. Software Eng., vol. 11, no. 1, Jan. 1985.
[43] P.Z. Kolano, "ASTRAL Software Development Environment User's Manual," TRCS96-31, Dept. of Computer Science, Univ. of California, Santa Barbara, July 1996.
[44] R. Koymans, R. Kuiper, and E. Zijlstra, "Specifying Message Passing and Real-Time Systems with Real-Time Temporal Logic," ESPRIT '87 Achievement and Impact, NorthHolland, 1987.
[45] R. Koymans, "Specifying Message Passing and Time-Critical Systems with Temporal Logic," PhD thesis, Eindhoven Univ. of Tech nology, 1989.
[46] R. Koymans and W.P. de Roever, "Examples of a Realtime Temporal Logic Specification," Lecture Notes in Computer Science 207.Berlin: Springer-Verlag, 1985.
[47] R. Abbott and H. Garcia-Molina, "Scheduling I/O Requests with Deadlines: A Performance Evaluation," Proc. IEEE Real-Time Systems Symp., pp. 113-124, 1990.
[48] B. Liskov, "Practical Uses of Synchronized Clocks in Distributed Systems," Distributed Computing, vol. 6, no. 4, pp. 211-219, 1993.
[49] F. Lagnier, P. Raymond, and C. Dubois, "Formal Verification of Critical Systems Written in Saga/Lustre," Workshop of Formal Methods, Modeling and Simulation for System Eng., St. Quentin en Yvelines (F), Feb. 1995.
[50] A. Morzenti, D. Mandrioli, and C. Ghezzi, “A Model-Parametric Real-Time Logic,” ACM Trans. Programming Languages and Systems, vol. 14, no. 4, pp. 521-573, Oct. 1992.
[51] P. Merlin and D.J. Farber, Recoverability of Communication Protocols IEEE Trans. Comm., vol. 24, no. 9, Sept. 1976.
[52] R. Milner, "Calculi for Synchroni and Asynchroni," Theoretical Computer Science, vol. 25, 1983.
[53] A. Morzenti and P. San Pietro, “Object-Oriented Logic Specifications of Time Critical Systems,” ACM Trans. Software Eng. and Methodology, vol. 3, no. 1, pp. 56-98, Jan. 1994.
[54] J. Ostroff, Temporal Logic for Real-Time Systems. John Wiley and Sons, 1989.
[55] A. Pnueli, "The Temporal Semantics of Computer Programs," Theoretical Computer Science, vol. 13, 1981.
[56] W.J. Quirk, Verification and Validation of Real-Time Software.Berlin: Springer-Verlag, 1985.
[57] I. Suzuki,“Formal analysis of the alternating bit protocol by temporal Petrinets,” IEEE Transactions on Software Engineering, vol. 16, no. 11, Nov. 1990.
[58] Y. Wang, "Realtime Behavior of Asynchronous Agents," Lecture Notes in Computer Science 458, pp. 502-520. Springer-Verlag, 1990.
[59] J. Zwiers, "Compositionality, Concurrency, and Partial Correctness," Lecture Notes in Computer Science 321.Berlin: Springer-Verlag, 1989.

Index Terms:
Formal methods, formal specification and verification, assertions, temporal logic, realtime systems, timing requirements, state machines, composability, ASLAN, TRIO.
Citation:
Alberto Coen-Porisini, Carlo Ghezzi, Richard A. Kemmerer, "Specification of Realtime Systems Using ASTRAL," IEEE Transactions on Software Engineering, vol. 23, no. 9, pp. 572-598, Sept. 1997, doi:10.1109/32.629494
Usage of this product signifies your acceptance of the Terms of Use.