This Article 
 Bibliographic References 
 Add to: 
Specification and Design of Transactions in Information Systems: A Formal Approach
August 1991 (vol. 17 no. 8)
pp. 814-829

In conventional information systems development, consistency between requirements specifications and design is achieved by manual checking. The application of the transformational paradigm to the specification and design phases is proposed. Requirements are expressed in the ADISSA notation, using the ADISSA method, a transaction-oriented refinement of structured systems analysis. The control part of a transaction is transformed into a formal specification, the FSM (finite state machine) transaction, by applying a set of rules. The design stage is realized by an algorithm which compares the FSM transaction into simpler transactions and implements them with a hierarchical set of finite-state machines. Consistency between the formal specification and the result of the design is achieved by proving that the latter has the same behavior as the former.

[1] T. DeMarco,Structured Analysis and System Specification. New York: Yourdon, 1978.
[2] C. Gane and T. Sarson,Structured Systems Analysis: Tools and Techniques. Englewood Cliffs, NJ: Prentice-Hall, 1979.
[3] Yourdon, E., and L.L. Constantine,Structured Design: Fundamentals Discipline of Computer Programs and Systems Design, Yourdon Press, New York, 1978.
[4] H. D. Mills, "Structured programming: retrospect and prospect,"IEEE Software, pp. 58-66, Nov. 1986.
[5] R. Balzer, "Transformational implementation: an example,"IEEE Trans. Software Eng., vol. SE-7, pp. 3-14, Jan. 1981.
[6] P. Shoval, "ADISSA: architectural design of information systems based on structured analysis,"Inform: Syst., vol. 13, pp. 193-210, 1988.
[7] F. Lustman, P. Mercier, and L. Gratton, "A dialog-based architecture for interactive information systems,"Data Base, vol. 16, pp. 18-24, Spring 1985.
[8] P. Zave, "An operational approach to requirements for embedded systems,"IEEE Trans. Software Eng., vol. SE-8, pp. 250-269, May 1982.
[9] B. Liskov, "Structure of distributed programs" (invited lecture), presented at the 12th Int. Conf. Software Eng., Nice, France, Mar. 26-30, 1990.
[10] G. Babin, "Implantation exacte de transactionsàl'aide de machines séquentielles," Master's thesis, Universitéde Montréal, Apr. 1989.
[11] P. Shoval and O. Manor, "Software engineering tools supporting ADISSA methodology for systems analysis and design,"Inform. Software Technol., vol. 32, no. 5, pp. 357-369, June 1990.
[12] P. Shoval and M. Even-Chaime, "ADDS: a system for automatic database schema design based on the binary relationship model,"Data Knowledge Eng., vol. 2, pp. 123-144, 1987.
[13] S. R. Faulk and D. L. Parnas, "On synchronization in hard-real-time systems,"Commun. ACMvol. 31, no. 3, Mar. 1988.
[14] R. E. A. Mason and T. T. Carey, "Prototyping interactive information systems,"Commun. ACM, vol. 26, no. 5, pp. 347-354, May 1983.

Index Terms:
formal approach; conventional information systems development; requirements specifications; manual checking; transformational paradigm; ADISSA notation; transaction-oriented refinement; structured systems analysis; formal specification; FSM; finite state machine; hierarchical set; data integrity; finite automata; formal specification; structured programming; systems analysis; transaction processing
G. Babin, F. Lustman, P. Shoval, "Specification and Design of Transactions in Information Systems: A Formal Approach," IEEE Transactions on Software Engineering, vol. 17, no. 8, pp. 814-829, Aug. 1991, doi:10.1109/32.83916
Usage of this product signifies your acceptance of the Terms of Use.