This Article 
 Bibliographic References 
 Add to: 
Querying of Executable Software Specifications
August 1992 (vol. 18 no. 8)
pp. 705-716

The availability of executable specification languages allows testing to be carried out soon after or concurrently with the requirements specification phase. In addition, it becomes possible to use these languages for rapid prototyping, making it possible to gather information on properties of the specified target system including its behavior in response to external events. The inspection of software behavior is viewed as the querying of executable specifications. A language RSQ is defined for the purpose of constructing queries against executable specifications expressed in RSF, a language for the description of systems with time constraints. A query is able to single out a subclass of possible behaviors based on properties supplied by the query. The integration of RSQ with RSF enhances the analytical abilities of the software designer and developer.

[1] M. Abadi and Z. Manna, "Temporal logic programming," inProc. 1987 Symp. on Logic Programming, IEEE Computer Society Press, 1987.
[2] B. Auernheimer and R. A. Kemmerer, "RT-ASLAN: A specification language for real time systems,"IEEE Trans. Software Eng., vol. SE-12, pp. 879-889, Sept. 1986.
[3] R. Balzer, T. E. Cheatham, and C. Green, "Software technology in 1990's: Using a new paradigm,"IEEE Computer, pp. 39-45, Nov. 1983.
[4] B. Belkhouche and J. E. Urban, "Direct implementation of abstract data type from abstract specifications,"IEEE Trans. Software Eng., vol. SE- 12, pp. 649-661, May 1986.
[5] G. Berry and L. Cosserat, "The ESTEREL synchronous programming language and its mathematical semantics," Seminar in Concurrency, LNCS 197, 1985.
[6] D. M. Berry and J. M. Wing, "Specifying and prototyping: Some thoughts on why they are successful," inFormal Methods and Software Development. Tapsoft Berlin, vol. 2, Mar. 1985.
[7] B. W. Boehm, T. Gray Seewaldt, "Prototyping versus specifying, A multiproject experiment,"IEEE Trans. Software Eng., vol. SE-10, May 1984.
[8] B. W. Boehm, "Seven basic principles of software engineering,"J. Systems and Software, vol. 3, pp. 3-24, Mar. 1983.
[9] M. C. Browne, E. M. Clarke, D. L. Dill, and B. Mishra, "Automatic verification of sequential circuits using temporal logic,"IEEE Trans. Computers, vol. C-35, pp. 1035-1044, Dec. 1986.
[10] R. Budde, Ed., "Approaches to prototyping," inProc. Working Conf. on Prototyping. New York: Springer, 1984.
[11] "The CAML Reference Manual," INRIA-ENS, INRIA Domaine de voluceau, Roquencqourt, Mar. 1989.
[12] F. Clocksin and S. Mellish,Programming in Prolog. Berlin: Springer Verlag, 1981.
[13] M. Degl'innocenti, G. Ferrari, G. Pacini, and F. Turini, "RSF: A formalism for executable requirement specifications,"IEEE Trans. Software Eng., vol. SE-16, pp. 1235-1246, Nov. 1990.
[14] M. Eisenstadt and M. Brayshaw, "The transparent prolog macine (TPM): An execution model and graphical debugger for logic programming,"J. Logic Programming, pp. 277-342, 1988.
[15] F. Garzotto, C. Ghezzi, D. Mandrioli, and A. Morzenti, "On the specification of real time systems using logic programming," inProc. First European Software Eng. Conf., Strasbourg, Springer Verlag, LNCS 289, 1987.
[16] N. Gehani and A. D. McGettrick, Eds.,Software Specification Techniques. Reading, MA: Addison Wesley, 1986.
[17] C. P. Gerrard, D. Coleman, and R. M. Gallimore, "Formal specification and design time testing,"IEEE Trans. Software Eng., vol. SE-16, pp. 1-11, Jan. 1990.
[18] M. Graf, "A visual environment for the design of distributed systems," in Proc.IEEE Workshop on Visual Languages, Linkoping, Sweden, pp. 330-344, Aug. 1987.
[19] M. Hamilton and S. Zeldin, "The functional life cycle model and its automation: USE.IT,"J. Systems and Software, vol. 3, pp. 25-62, Mar. 1983.
[20] D. Harelet al., "Statemate: A working environment for the development of complex reactive systems,"IEEE Trans. Software Eng., vol. SE-16, pp. 403-414, Apr. 1990.
[21] I. J. Hayes, "Specification-directed module testing,"IEEE Trans. Software Eng., vol. SE-12, pp. 124-133, Jan. 1986.
[22] P. Henderson, "Functional programming, formal specifications, and rapid prototyping,"IEEE Trans. Software Eng., vol. SE-12, pp. 241-250, Feb. 1986.
[23] M. A. Holliday and M. K. Vernon, "A generalized timed Petri net model for performance analysis,"IEEE Trans. Software Eng., vol. SE-13, no. 12, pp. 1297-1310, Dec. 1987.
[24] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in real-time systems,"IEEE Trans. Software Eng., vol. SE-12, no. 9, pp. 890-904, Sept. 1986.
[25] C. Jard, J. F. Monin, and R. Groz, "Development of VEDA, a prototyping tool for distributed algorithms,"IEEE Trans. Software Eng., vol. SE-14, pp. 339-351, Mar. 1988.
[26] R. A. Kemmerer, "Testing formal specifications to detect design errors,"IEEE Trans. Software Eng., vol. SE-11, pp. 32-43, Jan. 1985.
[27] R. Koymans and W. P. de Roever, "Examples of a real time temporal logic specification," LNCS 207, Springer Verlag, 1985.
[28] R. Kowalski and M. Sergot, "A logic based calculus of events,"New Generation Computing, Feb. 1986.
[29] H. J. Komorowski and J. Maluszynski, "Logic programming and rapid prototyping,"Science of Computer Programming, no. 9, pp. 179-205, 1987.
[30] C. H. Kung, "Conceptual modeling in the context of software development,"IEEE Trans. Software Eng., vol. SE-15, pp. 1176-1178, Oct. 1989.
[31] L. Lamport,What Good is Temporal Logic. IFIP 83, R. E. A. Mason, Ed. Elsevier Science, North Holland, 1983.
[32] R. Lee, H. Coelho, and J. C. Cotta, "Temporal inferencing on administrative data bases,"Inform. Syst., vol. 10, 1985.
[33] T. G., Lewis, F. Handloser, S. Bose, and S. Yang, "Prototypes from standard user interface management systems,"IEEE Computer, pp. 51-60, May 1989.
[34] Luqi, V. Bertzins, and R. Yeh, "A prototyping language for real time software,"IEEE Trans. Software Eng., vol. SE-14, pp. 1409-1423, Oct. 1988.
[35] R. Milner, "A proposal for standard ML,"Conf. Record of the ACM Symp. LISP and Functional Programming, Aug. 1984.
[36] G. Pacini and F.Turini, "Animation of software requirements,"Industrial Software Technology, R.J. Mitchell, Ed. London: P. Peregrinus Ltd., 1987.
[37] A. Pnueli, "Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of CurrentTrends," inCurrent Trends in Concurrency: Overviews and Tutorials. W.-P. de Roever and G. Rozenberg, eds., Lecture Notes in Computer Science 224, Springer-Verlag, N.Y., 1986, pp. 510-584.
[38] C. V. Ramamoorthy and G. S. Ho, "Performance evaluation of asynchronous systems using Petri nets,"IEEE Trans. Software Eng., vol. SE-6, pp. 440-449, Sept. 1980.
[39] D. P. Sidhu and C. S. Crall, "Executable logic specification for protocol service interfaces,"IEEE Trans. Software Eng., vol. SE-14, pp. 98-121, Jan. 1988.
[40] C. Sterling and E. Shapiro,The Art of Prolog: Advanced Programming Techniques. Cambridge, MA: MIT Press, 1986.
[41] R. B. Terwilliger and R. H. Campbell, "PLEASE: Executable specifications for incremental software development,"J. Systems and Software, pp. 97-112, 1989.
[42] P. Zave and W. Schell, "Salient features of an executable specification language and its environment,"IEEE Trans. Software Eng., vol. SE-12, no. 2, pp. 312-325, Feb. 1986.

Index Terms:
querying; executable software specifications; specification languages; requirements specification phase; rapid prototyping; external events; language RSQ; RSF; time constraints; software designer; formal specification; query languages; software prototyping; specification languages
G. Nota, G. Pacini, "Querying of Executable Software Specifications," IEEE Transactions on Software Engineering, vol. 18, no. 8, pp. 705-716, Aug. 1992, doi:10.1109/32.153380
Usage of this product signifies your acceptance of the Terms of Use.