
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Alberto CoenPorisini, Carlo Ghezzi, Richard A. Kemmerer, "Specification of Realtime Systems Using ASTRAL," IEEE Transactions on Software Engineering, vol. 23, no. 9, pp. 572598, September, 1997.  
BibTex  x  
@article{ 10.1109/32.629494, author = {Alberto CoenPorisini and Carlo Ghezzi and Richard A. Kemmerer}, title = {Specification of Realtime Systems Using ASTRAL}, journal ={IEEE Transactions on Software Engineering}, volume = {23}, number = {9}, issn = {00985589}, year = {1997}, pages = {572598}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.629494}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Specification of Realtime Systems Using ASTRAL IS  9 SN  00985589 SP572 EP598 EPD  572598 A1  Alberto CoenPorisini, A1  Carlo Ghezzi, A1  Richard A. Kemmerer, PY  1997 KW  Formal methods KW  formal specification and verification KW  assertions KW  temporal logic KW  realtime systems KW  timing requirements KW  state machines KW  composability KW  ASLAN KW  TRIO. VL  23 JA  IEEE Transactions on Software Engineering ER   
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, “ModelChecking for RealTime Systems,” Proc. Fifth Symp. Logic in Computer Science, June 1990.
[2] R. Alur and D.L. Dill,“The theory of timed automata,” RealTime: Theory in Practice, J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rosenberg, eds., Lecture Notes in Computer Science #600, pp. 2873. SpringerVerlag, 1991.
[3] R. Alur, T. Feder, and T. Henzinger, "The Benefits of Relaxing Punctuality," Proc. 10th ACM Symp. Principles of Distributed Computing, pp. 139152, 1991.
[4] B. Auernheimer and R.A. Kemmerer, "ASLAN User's Manual," TRCS8410, 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, “Rtaslan: A Specification Language for RealTime Systems,” IEEE Trans. Software Eng., vol. 12, no. 9, Sept. 1986.
[7] M. Abadi and L. Lamport, “An OldFashioned Recipe for Real Time,” Proc. REX Workshop, RealTime Theory in Practice, pp. 127, June 1991.
[8] M. Abadi and L. Lamport, "Conjoining Specifications," ACM Trans. Programming Languages and Systems, Vol. 17, No. 3, May 1995, pp. 507534.
[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. CoenPorisini, 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. 261322.
[12] F. Boussinot and R. de Simone, "The Esterel Language," Another Look at Real Time Programming, Proc. IEEE, vol. 79, pp. 1,2931,304, 1991.
[13] K.M. Chandy and J. Misra, Parallel Program Design—A Foundation. AddisonWesley, 1988.
[14] A. CoenPorisini and R.A. Kemmerer, "The Composability of ASTRAL Realtime Specifications," Proc. Int'l Symp. Software Testing and Analysis,Cambridge, Mass., July 1993.
[15] A. CoenPorisini, R. Kemmerer, and D. Mandrioli, “A Formal Framework for ASTRAL Intra Level Proof Obligations,” IEEE Trans. Software Eng., vol. 20, no. 8, pp. 548561, Aug. 1994.
[16] A. CoenPorisini, R.A. Kemmerer, and D. Mandrioli, "A Formal Framework for ASTRAL Interlevel Proof Obligations," Proc. Fifth European Software Eng. Conf.,Barcelona, Spain, Sept. 1995.
[17] A. CoenPorisini, P. San Pietro, and R. Kemmerer, "Formal Semantics Definition for ASTRAL," Report No. TRCS 9415, Dept. of Computer Science, Univ. of California, Santa Barbara, Sept. 1994.
[18] B. Dasarathy, "Timing Constraints of RealTime 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. 374402, 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. 1527, 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. 653671, Dec. 1994.
[22] S.R. Faulk and D.L. Parnas, On Synchronization in HardRealTime Systems Comm. ACM, vol. 31, pp. 274287, Mar. 1988.
[23] M. Felder and A. Morzenti, “Validating RealTime Systems by HistoryChecking 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 RealTime 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. 5160, May 1991.
[26] P. Le Guernic, T. Gautier, M. Le Borgne, and C. Le Maire, "Programming RealTime 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 RealTime Systems," IEEE Trans. Software Eng., vol. 18, no. 9, pp. 768784, 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 RealTime Systems," J. Systems and Software, vol. 12, no. 2, pp. 107123, May 1990.
[32] H. Gomaa, "Software Design Methods for the Design of LargeScale RealTime Systems," J. Systems and Software, vol. 25, no. 2, pp. 127146, 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 DataFlow Programming Language LUSTRE," Proc. IEEE, vol. 79, no. 9, pp. 1,3051,320, Sept. 1991.
[35] C. Heitmeyer and N. Lynch, "The Generalized Railroad Crossing: A Case Study in Formal Verification of RealTime Systems," Proc. RealTime Systems,San Juan, Puerto Rico, Dec. 1994.
[36] D. Harel,H. Lachover,A. Naamad,A. Pnueli,M. Politi,R. Sherman,A. ShtulTrauring,“Statemate: A working environment for the development of complex reactive systems,” Proc. 10th Int’l Conf. Software Eng. (ICSE 10), IEEE Computer Soc., pp. 396406, 1988.
[37] C. Ratel, N. Halbwachs, and P. Raymond, "Programming and Verifying RealTime Systems by Means of the Synchronous DataFlow Language LUSTRE," IEEE Trans. Software Eng., vol. 18, no. 9, pp. 785793, Sept. 1992.
[38] D.J. Hatley and I.A. Pirbhai,Strategies for RealTime System Specification, Dorset House, 1987.
[39] M.S. Jaffe and N.G. Leveson, "Completeness, Robustness, and Safety in RealTime 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 realtime systems,”IEEE Trans. Software Eng., vol. SE12, pp. 890–904, Sept. 1986.
[41] F. Jahanian and A.K. Mok, "Modechart: A Specification Language for RealTime Systems," IEEE Trans. Software Eng., vol. 20, no. 10, pp. 879889, 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," TRCS9631, Dept. of Computer Science, Univ. of California, Santa Barbara, July 1996.
[44] R. Koymans, R. Kuiper, and E. Zijlstra, "Specifying Message Passing and RealTime Systems with RealTime Temporal Logic," ESPRIT '87 Achievement and Impact, NorthHolland, 1987.
[45] R. Koymans, "Specifying Message Passing and TimeCritical 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: SpringerVerlag, 1985.
[47] R. Abbott and H. GarciaMolina, "Scheduling I/O Requests with Deadlines: A Performance Evaluation," Proc. IEEE RealTime Systems Symp., pp. 113124, 1990.
[48] B. Liskov, "Practical Uses of Synchronized Clocks in Distributed Systems," Distributed Computing, vol. 6, no. 4, pp. 211219, 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 ModelParametric RealTime Logic,” ACM Trans. Programming Languages and Systems, vol. 14, no. 4, pp. 521573, 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, “ObjectOriented Logic Specifications of Time Critical Systems,” ACM Trans. Software Eng. and Methodology, vol. 3, no. 1, pp. 5698, Jan. 1994.
[54] J. Ostroff, Temporal Logic for RealTime 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 RealTime Software.Berlin: SpringerVerlag, 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. 502520. SpringerVerlag, 1990.
[59] J. Zwiers, "Compositionality, Concurrency, and Partial Correctness," Lecture Notes in Computer Science 321.Berlin: SpringerVerlag, 1989.