[en] A framework is developed for studying the implementation process, as a stepwise process in which an abstract specification is successively transformed to reach a final compilable specification adapted to the computer environment. In this context, an implementation relation is referred to as the relation which should link any ``valid'' implementation to its abstract formal specification. In other words, the implementation relation is intended to express formally the notion of validity. Our framework allows the exact characterization of the transformations which may take place at each step for a given implementation relation. This framework is essential for dealing with non-transitive implementation relations. In the second part of the paper, these results are exemplified in LOTOS on some existing relations, and an apparent paradox is presented. Some new results about these relations are also derived.
Disciplines :
Computer science
Author, co-author :
Leduc, Guy ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Réseaux informatiques
Language :
English
Title :
A Framework Based on Implementation Relations for Implementing LOTOS Specifications
scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.
Bibliography
Abadi, Lamport (1988) The existence of refinement mappings. Proc. 3rd Annual Symposium on Logic in Computer Science , Edinburg, Scotland; 165-175.
Bergstra, Klop (1985) Algebra of communicating processes with abstraction. Theoret. Comput. Sci. 37:77-121.
Blyth, Dubuis, Hansson, Juanole, Kapus-Kolar, Kerner, Leduc, Le Moli, Lombardo, Marchena, Orth, Pavon, Pehrson, Tienari, Vogt (1988) Architectural and behavioural modelling in computer communication. Proc. IFIP WG10.3 Conference , M.H Barton, E.L Dagless, G.L Reijns, Amsterdam, The Netherlands, 5–7 October 1987, Distributed Processing, North-Holland, Amsterdam; 53-70.
Brookes, Hoare, Roscoe (1984) A theory of communicating sequential processes. J. ACM 31(3):560-599.
Bogaards (1989) LOTOS supported system development. Proc. 1st International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols—FORTE 88 , K.J Turner, Stirling, Scotland, 6–9 September 1988, Formal Description Techniques, North-Holland, Amsterdam; 279-294.
Bolognesi, Brinksma (1987) Introduction to the ISO specification language LOTOS. Comput. Networks ISDN Systems 14:25-29.
van Eijk, Vissers, Diaz The Formal Description Technique LOTOS , also reprinted in, North-Holland, Amsterdam; 1989, 23-73.
Brinksma (1987) On the existence of canonical testers. Report No. INF-87-5, Twente University of Technology, Department of Informatics, Enschede, The Netherlands; .
Brinksma (1988) A theory for the derivation of tests. Proc. IFIP WG6.1 8th International Symposium , S Aggarwal, K Sabnani, Atlantic City, NJ, USA, 7–10 June 1988, Protocol Specification, Testing, and Verification, North-Holland, Amsterdam; 8:63-74.
Brinksma, Scollo (1986) Formal notions of implementation and conformance in LOTOS. Report No. INF-86-13, Twente University of Technology, Department of Informatics, Enschede, The Netherlands; .
Brinksma, Scollo, Steenbergen (1987) Process specification, their implementations and their tests. Proc. IFIP WG6.1 6th International Workshop , B Sarikaya, G.V Bochmann, Montreal, Que., Canada, 10–13 June 1986, Protocol Specification, Testing, and Verification, North-Holland, Amsterdam; 6:349-360.
Chandy, Misra Parallel Program Design — A Foundation, Addison-Wesley, Reading, MA; 1989.
De Nicola (1987) Extensional equivalences for transition systems. Acta Inform. 24:211-237.
De Nicola, Hennessy (1984) Testing equivalences for processes. Theoret. Comput. Sci. 34:83-133.
Dubuis, Gotzhein, Hansson, Juanole, Kerner, Lahtinen, Leduc, Lombardo, Marchena, Orth, Palazzo, Pavon, Thalmann, Tienari, Tvrdy (1988) A framework for the taxonomy of synthesis and analysis activities in distributed system design. European Teleinformatics Conference (EUTECO 88) , R Speth, Vienna, Austria, 20–22 April 1988, Research into Networks and Distributed Applications, North-Holland, Amsterdam; 859-871.
Hennessy Algebraic Theory of Processes, MIT Press, Cambridge, MA; 1988.
ISO IS 8807 (1989) Information Processing Systems—Open Systems Interconnection—LOTOS—A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. ISO/IEC-JTC1/SC21/WG1/FDT/C.
Lam, Shankar (1984) Protocol verification via projections. IEEE Transactions on Software Engineering 10(4):325-342.
Lamport (1983) Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems 5(2):190-222.
Larsen (1990) Modal specifications. Automatic Verification Methods for Finite State Systems, Lecture Notes in Comput. Sci. , J Sifakis, Springer, Berlin; 407:232-246.
Leduc (1990) On the role of implementation relations in the design of distributed systems. Agrégation Dissertation, University of Liège, Dept. Systèmes et Automatique, B28, Liège, Belgium.
Lynch, Fisher (1981) On describing the behavior and implementation of distributed systems. Theoret. Comput. Sci. 13:17-43.
Lynch, Tuttle (1987) Hierarchical correctness proofs for distributed algorithms. Proc. 6th ACM Symposium on Principles of Distributed Computing , Vancouver, B.C., Canada; 137-151.
Merritt (1989) Completeness theorems for automata. Report AT&T Bell Laboratories, Murray Hill, NJ.
Milner Communication and Concurrency, Prentice-Hall, Englewood Cliffs, NJ; 1989.
Park (1981) Concurrency and automata on infinite sequences. Theoretical Computer Science, Lecture Notes in Comput. Sci. , Springer, Berlin; 104:167-183.
Swartout, Balzer (1982) On the inevitable intertwinning of specification and implementation. Comm. ACM 25(7):438-440.
van Eijk (1990) Tools for LOTOS specification style transformations. Proc. IFIP TC6 2nd International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols—FORTE 89 , S.T Vuong, Vancouver, B.C., Canada, 5–8 December 1989, Formal Description Techniques, North-Holland, Amsterdam; 2:43-51.
van Glabeek (1981) The linear time-branching time spectrum. CONCUR '90, Theories of Concurrency: Unification and Extension, Lecture Notes in Comput. Sci. , J.C.M Baeten, J.W Klop, Springer, Berlin; 458:278-297.
Vissers, Scollo, van Sinderen (1988) Architecture and specification style in formal descriptions of distributed systems. Proc. IFIP WG6.1 8th International Symposium , S Aggarwal, K Sabnani, Atlantic City, NJ, USA, 7–10 June 1988, Protocol Specification, Testing, and Verification, North-Holland, Amsterdam; 8:189-204.
Similar publications
Sorry the service is unavailable at the moment. Please try again later.
This website uses cookies to improve user experience. Read more
Save & Close
Accept all
Decline all
Show detailsHide details
Cookie declaration
About cookies
Strictly necessary
Performance
Strictly necessary cookies allow core website functionality such as user login and account management. The website cannot be used properly without strictly necessary cookies.
This cookie is used by Cookie-Script.com service to remember visitor cookie consent preferences. It is necessary for Cookie-Script.com cookie banner to work properly.
Performance cookies are used to see how visitors use the website, eg. analytics cookies. Those cookies cannot be used to directly identify a certain visitor.
Used to store the attribution information, the referrer initially used to visit the website
Cookies are small text files that are placed on your computer by websites that you visit. Websites use cookies to help users navigate efficiently and perform certain functions. Cookies that are required for the website to operate properly are allowed to be set without your permission. All other cookies need to be approved before they can be set in the browser.
You can change your consent to cookie usage at any time on our Privacy Policy page.
