Structured Occurrence Nets: A Formalism for Aiding System Failure Prevention and Analysis Techniques

• Autorzy: Koutny, M. , Randell, B.
• Języki publikacji: EN

Abstrakty

EN

This paper introduces the concept of a "structured occurrence net", which as its name indicates is based on that of an "occurrence net", a well-established formalism for an abstract record that represents causality and concurrency information concerning a single execution of a system. Structured occurrence nets consist of multiple occurrence nets, associated together by means of various types of relationship, and are intended for recording or predicting, either the actual behaviour of complex systems as they communicate and evolve, or evidence that is being gathered and analysed concerning their alleged past behaviour. We provide a formal basis for the new formalism and show how it can be used to gain better understanding of complex fault-error-failure chains (i) among co-existing communicating systems, (ii) between systems and their sub-systems, and (iii) involving systems that are controlling, creating ormodifying other systems. We then go on to discuss how, with appropriate tools support, perhaps using extended versions of existing tools, structured occurrence nets could form a basis for improved techniques of system failure prevention and analysis.

Słowa kluczowe

EN

failures; error; faults; dependability; judgemen; occurrence nets; abstraction; formal analysis

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 97, nr 1/2
• Strony: 41-91
• Opis fizyczny: Bibliogr. 24 poz., wykr.

Twórcy

autor

Koutny, M.

autor

Randell, B.

• School of Computing Science, Newcastle University, Newcastle upon Tyne NE1 7RU, U.K.,

Bibliografia

• [1] A.Avizienis, J.-C.Laprie, B.Randell and C.Landwehr (2004). Basic Concepts and Taxonomy of Dependable and Secure Computing. IEEE Trans. on Dep. and Sec. Comp. 1, 11-33.
• [2] P.Baldan, T.Chatain, S.Haar and B.K¨onig (2008). Unfolding-Based Diagnosis of Systems with an Evolving Topology. Proc. of CONCUR'08, LNCS 5201, 203-217.
• [3] E. Best and R. Devillers (1988). Sequential and Concurrent Behaviour in Petri Net Theory. Theoretical Computer Science 55, 87-136.
• [4] E.Best and B.Randell (1981). A FormalModel of Atomicity in Asynchronous Systems. Acta Informatica 16, 93-124.
• [5] J.Esparza and K.Heljanko (2008). Unfoldings: A Partial-Order Approach to Model Checking. Springer.
• [6] J.Esparza, S.R¨omer and W.Vogler (2002). An Improvement of McMillan's Unfolding Algorithm. Formal Methods in System Design 20, 285-310.
• [7] P.Gladyshev and A.Patel (2005). Formalising Event Time Bounding in Digital Investigations. International Journal of Digital Evidence 4.
• [8] A.W.Holt, R.M.Shapiro, H.Saint and S.Marshall (1968). Information System Theory Project. Report RADCTR-68-305, US Air Force, Rome Air Development Center.
• [9] J.Keppens and B.Schafer (2006). Knowledge Based Crime Scenario Modelling. Expert Syst. Appl. 30, 203-222.
• [10] V.Khomenko and M.Koutny (2007). Verification of Bounded Petri Nets Using Integer Programming. Formal Methods in System Design 30, 143-176.
• [11] V.Khomenko, M.Koutny and A.Niaouris (2006). Applying Petri Net Unfoldings for Verification of Mobile Systems. Report CS-TR 953, Newcastle University.
• [12] V.Khomenko,M.Koutny and A.Yakovlev (2006). Logic Synthesis for Asynchronous Circuits Based on STG Unfoldings and Incremental SAT. Fundamenta Informaticae 70, 49-73.
• [13] H.C.M.Kleijn and M.Koutny (2004). Process Semantics of General Inhibitor Nets. Information and Computation 190, 18-69.
• [14] D.Koppad, D.Sokolov, A.Bystrov and A.Yakovlev (2006). Online Testing by Protocol Decomposition. Proc. of IOLTS'06, IEEE CS Press, 263-268.
• [15] P.B.Ladkin (2000). Causal Reasoning about Aircraft Accidents. Proc. of SAFECOMP 2000, LNCS 1943, 344-360.
• [16] S.Lenk (1994). Extended Timing Diagrams as a Specification Language. Proc. of European Design Automation, IEEE Computer Society Press, 28-33.
• [17] S.Mauw (1996). The Formalization ofMessage Sequence Charts. Computer Networks and ISDN Systems 28, 1643-1657.
• [18] K.L.McMillan (1995). A Technique of State Space Search Based on Unfoldings. Formal Methods in System Design 6, 45-65.
• [19] S.Melzer and S.R¨omer (1997). Deadlock Checking Using Net Unfoldings. Proc. of CAV'97, LNCS 1254, 352-363.
• [20] P.M.Merlin and B.Randell (1978). State Restoration in Distributed Systems. Proc. of FTCS-8, IEEE Computer Society Press, 129-134.
• [21] B.Randell and M.Koutny (2007). Failures: Their Definition, Modelling and Analysis. Proc. of ICTAC'07, LNCS 4711, 260-274.
• [22] G.Rozenberg and J.Engelfriet (1998). Elementary Net Systems. Proc. of Advances in Petri Nets. Lectures on Petri Nets I: Basic Models, LNCS 1491, 12-121.
• [23] F.J.Thayer, J.C.Herzog and J.D.Guttman (1999). Strand Spaces: Proving Security Protocols Correct. Journal of Computer Security 7, 191-230.
• [24] http://www.rail-reg.gov.uk/upload/pdf/incident-ladbrokegrove-ladbroke-optim.pdf