Proving Nets Correct via Cause-Effect Structures (An Experiment)

• Autorzy: Czaja L.
• Języki publikacji: EN

Abstrakty

EN

Proving safety and liveness of parallel systems is of unquestionable importance in system construction activity. A proof method for systems represented by nets (cause-effect structures and Petri nets) is proposed. Its outline is the following. (1) Let a problem specification as a formal theory i.e. a language system with specific relation symbols (operations, in particular), axioms and first-order inference rules be given. For each symbol introduce a class of atomic c-e structures (counterpart of Petri net transitions) to be the symbol's operational representative. (2) Using algebraic calculus of cause-effect structures, construct - from the atoms - a c-e structure and equivalent net intended to behave in accordance with the axioms (a mechanical step); (3) From the cause-effect structure just constructed, infer an algebraic structure and prove it to be a model (in terms of model theory) of the axiomatic system specifying the problem.

Słowa kluczowe

EN

cause-effect structures; Petri net; specification; correctness; model theory

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 54, nr 2,3
• Strony: 165--183
• Opis fizyczny: bibliogr. 11 poz.

Twórcy

autor

Czaja L.

• Institute of Informatics Warsaw University ul. Banacha 2 02-097 Warsaw, Poland,

Bibliografia

• [Cza 1988] Czaja L., Cause-Effect Structures, Information Processing Letters, 26, Jan.1988, pp. 313-319
• [Cza 1993] Czaja L., Net Models of Abstract Data Types, Proceedings of CONCURRENCY, SPECIFI-CATION AND PROGRAMMING workshop, Nieborow, 1993, pp.85-116
• [Cza 1998] Czaja L., Cause-Effect Structures - Structural and Semantic Properties Revisited, Fundamenta Informaticae Vol. 33, N. 1, January 1998, pp. 17-42
• [Cza 2000] Czaja L., Elementarnye Prichinno-Sledstwennye Struktury (Russian), in SISTEMNAYA IN-FORMATIKA 7, NAUKA, 2000, pp. 7-81
• [Cza 2002] Czaja L., Elementary Cause-Effect Structures, Warsaw University Press 2002
• [Le-Pn-St 1981] Lehmann D., Pnueli A., Stavi J., Impartiality, justice, fairness: The ethics of concurrent termination, in Automata, Languages and Programming (S.Eve and D.Kariv eds.), LNCS 115, 1981, pp. 264-277
• [Mir-Sal 1987] Mirkowska G., Salwicki A., Algorithmic Logic, PWN - Polish Scientific Publishers and D. Reidel Publishing Company, Dordrecht/Boston/Lancaster/Tokyo, 1987
• [Pos 2003] Poslowski W., Private communication
• [Rac 1993] Raczunas M. Remarks on the equivalence of c-e structures and Petri nets, Information Proc. Letters, 45 (1993) pp. 165-169
• [Rei 1985] Reisig W., Petri Nets. An Introduction, Number 4 in EATCS Monographs on Theoretical Computer Science, Springer, Berlin-Heidelberg-New York, Tokyo, 1985
• [Rei 1994] Reisig W., Progress in Petri Nets, Humboldt Universitat zu Berlin, Informatik Bericht Nr.34, Mai 1994