Combining and Distributing Hierarchical Systems
It is possible with RAISE to specify and do most refinement in an applicative framework, and then transform the concrete applicative specification into an imperative sequential or concurrent one. This is a change from a style more appropriate to proof of refinement to a style more appropriate to implementation.
The resulting imperative specification is typically hierarchical, with upper levels calling the functions of lower ones. This paper presents a further stage of development in which the hierarchical structure is transformed into a distributed one, and components communicate asynchronously. This also allows “horizontal” communication between components of previously separate hierarchies.
A major design aim is to reuse the hierarchical specification, as far as possible extending the existing modules by standard, generic components. The method should achieve correctness by construction, and be amenable to quality control; it is an example of an engineering approach using standard components and standard assembly techniques.
The method is illustrated by collaborative work done between UNU/IIST and the Vietnamese Ministry of Finance in developing a specification of a national financial information system.
KeywordsFormal specification development refinement reuse restructuring distributed systems coordination software engineering
Unable to display preview. Download preview PDF.
- 1.The RAISE Method Group: The RAISE Development Method. BCS Practitioner Series. Prentice Hall, Englewood Cliffs (1995)Google Scholar
- 2.Dung, D.T., Chi, L.L., Thu, N.L., Nam, P.P., Lien, T.M., George, C.: Developing a Financial Information System. Technical Report 81, UNU/IIST, P.O.Box 3058, Macau (September 1996)Google Scholar
- 3.Dung, D.T., George, C., Huan, H.X., Nam, P.P.: A Financial Information System. Technical Report 115, UNU/IIST, P.O.Box 3058, Macau (July 1997)Google Scholar
- 5.Gerth, R., Kuiper, R., Segers, J.: Interface Refinement in Reactive Systems. In: Cleaveland Google Scholar
- 6.Meldal, S., Luckham, D.C.: Defining a Security Reference Architecture. Technical Report CSL-TR-97-728, Stanford University (June 1997)Google Scholar
- 7.Wegner, P.: Coordination as Constrained Interaction. In: Ciancarini and Hankin Google Scholar
- 8.Ciancarini, P., Hankin, C. (eds.): COORDINATION 1996. LNCS, vol. 1061. Springer, Heidelberg (1996)Google Scholar
- 10.The RAISE Language Group: The RAISE Specification Language. BCS Practitioner Series. Prentice Hall, Englewood Cliffs (1992)Google Scholar
- 11.Guttag, J.V.: Abstract data types and the development of data structures. CACM 20(6) (June 1977)Google Scholar
- 14.Milne, R.E.: Transforming Axioms for Data Types into Sequential Programs. In: Proceedings of 4th Refinement Workshop. Springer, Heidelberg (1991)Google Scholar