The proceedings contain 24 papers. The special focus in this conference is on Distributed Components, UML, Testing and Formal Methods. The topics include: Metamodelling and conformance checking with PVS;proving deadlo...
ISBN:
(纸本)3540418636
The proceedings contain 24 papers. The special focus in this conference is on Distributed Components, UML, Testing and Formal Methods. The topics include: Metamodelling and conformance checking with PVS;proving deadlock freedom in component-based programming;a real-time execution semantics for UML activity diagrams;strengthening UML collaboration diagrams by state transformations;on use cases and their relationships in the unified modelling-language;on the importance of inter-scenario relationships in hierarchical state machine design;library-based design and consistency checking of system-level industrial test cases;demonstration of an automated integrated testing environment for CTI systems;semantics of architectural specifications in CASL;a logic for the java modeling language JML;a formal object-oriented analysis for software reliability and specification and analysis of the AER/NCA active network protocol suite in real-time Maude.
Garbage collection relieves the programmer of the burden of managing dynamically allocated memory, by providing an automatic way to reclaim unneeded storage. This eliminates or lessens program errors that arise from a...
详细信息
We introduce [Ascr ]k, an extension of the action description language [Ascr ] (Gelfond and Lifschitz, 1993) to handle actions which affect knowledge. We use sensing actions to increase an agent's knowledge of the...
详细信息
We introduce [Ascr ]k, an extension of the action description language [Ascr ] (Gelfond and Lifschitz, 1993) to handle actions which affect knowledge. We use sensing actions to increase an agent's knowledge of the world and non-deterministic actions to remove knowledge. We include complex plans involving conditionals and loops in our query language for hypothetical reasoning. We also present a translation of [Ascr ]k domain descriptions into epistemic logic *** paper extends the results of the work first presented in Lobo et al. (1997).
Directional types form a type system for logic programs which is based on the view of a predicate as a directional procedure which, when applied to a tuple of input terms, generates a tuple of output terms. It is know...
详细信息
ISBN:
(纸本)3540672621
Directional types form a type system for logic programs which is based on the view of a predicate as a directional procedure which, when applied to a tuple of input terms, generates a tuple of output terms. It is known that directional-type checking wrt. arbitrary types is undecidable;several authors proved decidability of the problem wrt. discriminative regular types. In this paper, using techniques based on tree automata, we show that directional-type checking for logic programs wrt. general regular types is DEXPTIME-complete and fixed-parameter linear. The latter result shows that despite the exponential lower bound, the type system might be usable in practice.
Abstract interpretation theory has successfully been used for constructing algorithms to statically determine run-time properties of programs. Central is the notion of an abstract domain, describing certain properties...
详细信息
We prove some new results that simplify termination proofs for non-overlapping term rewriting systems. The first one is a refined modularity result (for not necessarily disjoint systems). The second, more important on...
详细信息
ISBN:
(纸本)1581132654
We prove some new results that simplify termination proofs for non-overlapping term rewriting systems. The first one is a refined modularity result (for not necessarily disjoint systems). The second, more important one, gives conditions under which the simplification of right-hand sides (using rules of the original system) is a sound preprocessing step, in the sense that termination of the original system is equivalent to termination of the simplified system, and that the equational theory is preserved. The proofs are based on some powerful structural properties known for non-overlapping systems. Finally, we show how to (partially) extend these results, in particular, to the case of conditional rewrite systems where we additionally treat simplification of conditions of rules. The presented results provide the theoretical basis for sound (and automatic) preprocessing steps when proving termination of (possibly conditional) non-overlapping rewrite systems and equational programs defined by such systems.
This paper formalises a semantics for statements and expressions (in sequential imperative languages) which includes non-termination, normal termination and abrupt termination (e.g. because of an exception, break, ret...
详细信息
ISBN:
(纸本)3540672613
This paper formalises a semantics for statements and expressions (in sequential imperative languages) which includes non-termination, normal termination and abrupt termination (e.g. because of an exception, break, return or continue). This extends the traditional semantics underlying e.g. Hoare logic, which only distinguishes termination and non-termination. An extension of Hoare logic is elaborated that includes means for reasoning about abrupt termination (and side-effects). It prominently involves rules for reasoning about while loops, which may contain exceptions, breaks, continues and returns. This extension applies in particular to Java. As an example, a standard pattern search algorithm in Java (involving a while loop with returns) is proven correct using the proof-tool PVS.
In this paper we show how model checking can be used for the verification of security protocols using a logic of belief. We model principals as processes able to have beliefs. The idea underlying the approach is to tr...
详细信息
ISBN:
(纸本)3540672826
In this paper we show how model checking can be used for the verification of security protocols using a logic of belief. We model principals as processes able to have beliefs. The idea underlying the approach is to treat separately the temporal evolution and the belief aspects of principals. Therefore, when we consider the temporal evolution, belief formulae are treated as atomic propositions;while the fact that principal A has beliefs about another principal B is modeled as the fact that A has access to a representation of B as a process. As a motivating example, we use the framework proposed to formalize the Andrew protocol.
We introduce and develop the notion of symmetric monoidal sketch. Every symmetric monoidal sketch generates a generic model. If the sketch is commutative and single-sorted, the generic model can be characterised as a ...
详细信息
ISBN:
(纸本)1581132654
We introduce and develop the notion of symmetric monoidal sketch. Every symmetric monoidal sketch generates a generic model. If the sketch is commutative and single-sorted, the generic model can be characterised as a free structured category on the small category 1. Moreover, there is a comonad Mods (S,-) on the category SymMons of small symmetric monoidal categories and strict symmetric monoidal functors such that the category of Mods(S,-)-coalgebras describes the above-mentioned structure. Given a commutative single-sorted sketch, the construction sending a small symmetric monoidal category to the category of models of the sketch in it provides a right adjoint to the forgetful functor from the category of coalgebras to SymMons. We investigate specific cases generated by the Eckmann-Hilton argument, which allows a simple characterisation of the constructions. This accounts for the various categories of wiring currently being investigated in modelling concurrency, as well as providing a basis for understanding the axiomatically generated categories in axiomatic domain theory and in presheaf models of concurrency.
暂无评论