Formal techniques for networked and distributed systems-- FORTE 2004 : 24th IFIP WG 6.1 International conference, Madrid, Spain, September 27-30, 2004 : proceedings

This book constitutes the refereed proceedings of the 24th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2004, held in Madrid, Spain, in September 2004. The 20 revised full papers presented together with 3 invited papers were carefully reviewed and selected from 54 submissions. Among the topics addressed are state-based specification, distributed Java objects, UML and SDL, algorithm verification, communicating automata, design recovery, formal protocol testing, testing and model checking, distributed real-time systems, formal composition, distributed testing, automata for ACTL, symbolic state space representation, pi-calculus, concurrency, Petri nets, routing protocol verification, and intrusion detection. Front Matter....Pages - A Logical Account of NGSCB....Pages 1-12 Composing Event Constraints in State-Based Specification....Pages 13-32 Formal Description Techniques and Software Engineering: Some Reflections after 2 Decades of Research....Pages 33-42 Parameterized Models for Distributed Java Objects....Pages 43-60 Towards the Harmonisation of UML and SDL....Pages 61-78 Localizing Program Errors for Cimple Debugging....Pages 79-96 Formal Verification of a Practical Lock-Free Queue Algorithm....Pages 97-114 Formal Verification of Web Applications Modeled by Communicating Automata....Pages 115-132 Towards Design Recovery from Observations....Pages 133-149 Network Protocol System Passive Testing for Fault Management: A Backward Checking Approach....Pages 150-166 Connectivity Testing Through Model-Checking....Pages 167-184 Fault Propagation by Equation Solving....Pages 185-198 Automatic Generation of Run-Time Test Oracles for Distributed Real-Time Systems....Pages 199-212 Formal Composition of Distributed Scenarios....Pages 213-228 Conditions for Resolving Observability Problems in Distributed Testing....Pages 229-242 Integrating Formal Verification with Mur φ of Distributed Cache Coherence Protocols in FAME Multiprocessor System Design....Pages 243-258 Witness and Counterexample Automata for ACTL....Pages 259-275 A Symbolic Symbolic State Space Representation....Pages 276-291 Introducing the Iteration in sPBC....Pages 292-308 Petri Net Semantics of the Finite π -Calculus....Pages 309-325 Symbolic Diagnosis of Partially Observable Concurrent Systems....Pages 326-342 Automatized Verification of Ad Hoc Routing Protocols....Pages 343-358 A Temporal Logic Based Framework for Intrusion Detection....Pages 359-376 Back Matter....Pages - This section gives a description of notions used throughout this study. Current achievements in developing action-centered ontologies are also discussed. 2.1 Ontologies In the context of information extraction and retrieval, different kinds of ontologies can be distinguished [15]: • Top-level ontologies describe very general concepts like space and time, not depending on a particular domain, • Domain ontologies and task ontologies describe the vocabulary related to a generic domain or kind of task, detailing the terms used in the top-level ontology, • Application ontologies describe the concepts that depend on the particular domain and task within a specific activity. Several investigations have been conducted to bring actions (tasks) to bear on - tologies. Among them are Chandrasekaran et al. [6] and Mizoguchi et al. [23] in the fields of AI and Knowledge Engineering. For the geospatial domain, Kuhn [21] and Raubal and Kuhn [26] have attempted to support human actions in ontologies for transportation. Acknowledging the importance of human actions in the geographic domain, a research workshop was held in 2002, bringing together experts from diff- ent disciplines to share the knowledge and work on this issue [1]. Camara [5], one of the workshop participants, has proposed that action-driven spatial ontologies are formed via category theory, for the case of emergency action plans.

This book constitutes the refereed proceedings of the 24th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2004, held in Madrid, Spain, in September 2004.

The 20 revised full papers presented together with 3 invited papers were carefully reviewed and selected from 54 submissions. Among the topics addressed are state-based specification, distributed Java objects, UML and SDL, algorithm verification, communicating automata, design recovery, formal prool testing, testing and model checking, distributed real-time systems, formal composition, distributed testing, automata for ACTL, symbolic state space representation, pi-calculus, concurrency, Petri nets, routing prool verification, and intrusion detection.

NGSCB ("Next-Generation Secure Computing Base", formerly known as "Palladium") integrates hardware and software components that aim to help in protecting data and processes against software attacks [8,9,14,15].