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.
In industrial practice it is much more common to control a process using logical control for discrete on/off states. As a result most industrial equipment designs use Programmable logic Controllers (PLCs). These contr...
详细信息
In industrial practice it is much more common to control a process using logical control for discrete on/off states. As a result most industrial equipment designs use Programmable logic Controllers (PLCs). These controllers support multiple control schemes such as Boolean logical control, sequential logic control, structured programming, linear controls, graphical interfaces, fuzzy logic, etc. A majority of engineering students are taught control of continuous systems using linear control theory. These courses often include topics such as step response and design of lead/lag controllers. In terms of the pedagogy, linear controls are less desirable for the mechanical engineering students because they are very difficult to implement in actual designs. The linear approach makes more sense for electrical engineering students who are familiar with the mathematical tools, and can implement the control system easily with common electronic components. This paper will describe a course, EGR 450 - Manufacturing Control Systems. The course includes lectures, laboratories and a project. This course uses rigorous design techniques and theoretical methods to teach industrial control to junior and senior engineering students. Topics include the design of basic combinatorial logic, sequential and state based logic, sensors and interfacing, communications and networking, analog I/O and PID control. This course has been very well received by students and local manufacturers.
This paper describes an experience in formal specification and fault tolerant behavior validation of a railway critical system. The work, performed in the context of a real industrial project, had the following main t...
详细信息
ISBN:
(纸本)3540672826
This paper describes an experience in formal specification and fault tolerant behavior validation of a railway critical system. The work, performed in the context of a real industrial project, had the following main targets: (a) to validate specific safety properties in the presence of byzantine system components or of some hardware temporary faults;(b) to design a formal model of a critical railway system at a right level of abstraction so that could be possible to verify certain safety properties and at the same time to use the model to simulate the system. For the model specification we used the PROMELA language, while the verification was performed using the SPIN model checker. Safety properties were specified by means of both assertions and temporal logic formulae. To make the problem of validation tractable in the SPIN environment, we used ad hoc abstraction techniques.
In this paper, we present a generic tool, called FMona, for expressing validation methods. we illustrate its use through the expression of the abstraction technique and its application to infinite or parameterized spa...
详细信息
ISBN:
(纸本)3540672826
In this paper, we present a generic tool, called FMona, for expressing validation methods. we illustrate its use through the expression of the abstraction technique and its application to infinite or parameterized space problems. After a review of the basic results concerning transition systems, we show how abstraction can be expressed within FMona and used to build a reduced system with decidable properties. The FMona tool is used to express the validation steps leading to synthesis of a finite abstract system;then SMV and/or Mona validate its properties.
We show how the problem of verifying parameterized systems can be reduced to the problem of determining the equivalence of goals in a logic program. We further show how goal equivalences can be established using induc...
详细信息
In the compositional verification of a concurrent system, one seeks to deduce properties of the system from properties of its constituent modules. This paper supplements our previous work on the same subject to provid...
详细信息
The proceedings contain 27 papers. The special focus in this conference is on programming Languages and Systems. The topics include: Functional nets;faithful translations between polyvariant flows and polymorphic type...
ISBN:
(纸本)3540672621
The proceedings contain 27 papers. The special focus in this conference is on programming Languages and Systems. The topics include: Functional nets;faithful translations between polyvariant flows and polymorphic types;on the expressiveness of event notification in data-driven coordination languages;flow-directed closure conversion for typed languages;directional type checking for logic programs;formalizing implementation strategies for first-class continuations;correctness of java card method lookup via logical relations;compile-time debugging of c programs working on trees;a calculus for compiling and linking classes;abstract domains for universal and existential properties;a type system for bounded space and functional in-place update-extended abstract information flow as typed process behaviour;implementing groundness analysis with definite boolean functions;the correctness of type specialisation;type classes with functional dependencies;proofnets for languages with explicit control;a calculus for link-time compilation;improving the representation of infinite trees to deal with sets of trees;on the translation of procedures to finite machines;a kleene analysis of mobile ambients;a 3-part type inference engine;first-class structures for standard ML;constraint-based inter-procedural analysis of parallel programs;alias types;polyvariant flow analysis with constrained types and on exceptions versus continuations in the presence of state.
Learning from examples is an important branch of inductive learning, and is also the bottleneck in concepts extraction of machine learning. Based on inductive learning theory this paper applies combinatorial optimizat...
详细信息
Learning from examples is an important branch of inductive learning, and is also the bottleneck in concepts extraction of machine learning. Based on inductive learning theory this paper applies combinatorial optimization method to setup the programming models of learning concepts of the prepositional logic formulas in the conjunctive normal form (CNF) and disjunctive normal form (DNF). Then, genetic algorithms (GA), specified to CNF learning, is designed. GA can find the multiple optimal solution in theory and practice, and experiments reveal that it runs more efficiently compared with heuristic algorithms of the generalisation-and-specialisation (GS) type.
Our approach of rule-based refinement(1) provides a formal description for the stepwise system development based on Petri nets. Rules with a left-hand and a right-hand side allow replacing subnets in a given algebraic...
详细信息
ISBN:
(纸本)3540672613
Our approach of rule-based refinement(1) provides a formal description for the stepwise system development based on Petri nets. Rules with a left-hand and a right-hand side allow replacing subnets in a given algebraic high-level net system. The extension of these rules supports the preservation of system properties. In this paper we extend the preservation of safety properties significantly. We define rules, that introduce new safety properties. In our new approach we propose first the verification of properties at the moment they can be expressed and then their preservation further on. Hence, properties can be checked as long as the system is still small. Moreover, introducing properties allows checking these for the relevant subpart only. Changes that are required later on can be treated the same way and hence preserve the system properties. Hence, we have made a step towards a formal technique for the stepwise system development during analysis and design.
暂无评论