首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到20条相似文献,搜索用时 31 毫秒
1.
Certain aspects of the behavior of concurrent systems are intrinsically probabilistic in nature, e.g., the behavior of imperfect communication media used in network protocols. We address the problem of expressing such behavior in an algebraic calculus for communicating systems. The introduction of probabilistic information in the calculus alleviates the problem of proving liveness, as proving liveness now amounts to proving that its probability is 1. A methodology for proving both safety and liveness is developed and used in proving the correctness of the Alternating Bit Protocol.  相似文献   

2.
We propose a timed broadcasting process calculus for wireless systems where time-consuming communications are exposed to collisions. The operational semantics of our calculus is given in terms of a labelled transition system. The calculus enjoys a number of desirable time properties such as (i) time determinism: the passage of time is deterministic; (ii) patience: devices will wait indefinitely until they can communicate; (iii) maximal progress: data transmissions cannot be delayed, they must occur as soon as a possibility for communication arises. We use our calculus to model and study MAC-layer protocols with a special emphasis on collisions and security. The main behavioural equality of our calculus is a timed variant of barbed congruence, a standard branching-time and contextually-defined program equivalence. As an efficient proof method for timed barbed congruence we define a labelled bisimilarity. We then apply our bisimulation proof-technique to prove a number of algebraic laws.  相似文献   

3.
We propose a process calculus to study the behavioural theory of Mobile Ad Hoc Networks. The operational semantics of our calculus is given both in terms of a Reduction Semantics and in terms of a Labelled Transition Semantics. We prove that the two semantics coincide. The labelled transition system is then used to derive the notions of (weak) simulation and bisimulation for ad hoc networks. The labelled bisimilarity completely characterises reduction barbed congruence, a standard branching-time and contextually-defined program equivalence. We then use our (bi)simulation proof method to formally prove a number of non-trivial properties of ad hoc networks.  相似文献   

4.
Cones and foci: A mechanical framework for protocol verification   总被引:1,自引:0,他引:1  
We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between data objects. Compared to the original cones and foci method from Groote and Springintveld, our method is more generally applicable, because it does not require a preprocessing step to eliminate τ-loops. We prove soundness of our approach and present a set of rules to prove the reachability of focus points. Our method has been formalized and proved correct using PVS. Thus we have established a framework for mechanical protocol verification. We apply this framework to the Concurrent Alternating Bit Protocol.
  相似文献   

5.
We present two complete systems for polymorphic types with sub- typing. One system is in the style of natural deduction, while another is a Gentzen-style sequent calculus system. We prove several meta- mathematical properties for these systems including cut elimination, subject reduction, coherence, and decidability of type reconstruction. Following the approach by J. Mitchell, the sequents are given a simple semantics using logical relations over applicative structures. The systems are complete with respect to this semantics. The logic which emerges from this paper can be seen as a successor to the original Hilbert style system proposed by J. Mitchell in 1988, and to the “half way” sequent calculus of G. Longo, K. Milsted, and S. Soloviev proposed in 1995.  相似文献   

6.
In 1981 Structural Operational Semantics (SOS) was introduced as a systematic way to define operational semantics of programming languages by a set of rules of a certain shape [G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981. Also published in: Journal of Logic and Algebraic Programming 60–61 (2004) 17–140]. Subsequently, the format of SOS rules became the object of study. Using so-called Transition System Specifications (TSS's) several authors syntactically restricted the format of rules and showed several useful properties about the semantics induced by any TSS adhering to the format. This has resulted in a line of research proposing several syntactical rule formats and associated meta-theorems. Properties that are guaranteed by such rule formats range from well-definedness of the operational semantics and compositionality of behavioral equivalences to security- and probability-related issues. In this paper, we provide an initial hierarchy of SOS rules formats and meta-theorems formulated around them.  相似文献   

7.
基于稳定模型的软件多样性与安全初探   总被引:1,自引:0,他引:1  
该文简要阐述了软件多样性与安全性的关系后,基于STABLEMODEL是逻辑程序的语义模型的观点,从软件与逻辑程序设计的关联出发,提出了用逻辑程序设计实现软件多样性的方法。论文首先介绍了逻辑程序中稳定模型的形成、定义、演算方法,通过逻辑程序与稳定模型之间存在的多对一的映射关系,产生软件的多样性。最后,通过具体的分析,提出了基于稳定模型的程序多样性演化方法,这一方法实现了从一个源程序到一系列等价程序的多样性演化,从而提高了系统的鲁棒性和安全性。  相似文献   

8.
Parsers, whether constructed by hand or automatically via a parser generator tool, typically need to compute some useful semantic information in addition to the purely syntactic analysis of their input. Semantic actions may be added to parsing code by hand, or the parser generator may have its own syntax for annotating grammar rules with semantic actions. In this paper, we take a functional programming view of such actions. We use concepts from the semantics of mostly functional programming languages and adapt them to give meaning to the actions of the parser. Specifically, the semantics is inspired by the categorical semantics of lambda calculi and the use of premonoidal categories for the semantics of effects in programming languages. This framework is then applied to our leading example, the transformation of grammars to eliminate left recursion. The syntactic transformation of left-recursion elimination leads to a corresponding semantic transformation of the actions for the grammar. We prove the semantic transformation correct and relate it to continuation passing style, a widely studied transformation in lambda calculi and functional programming. As an idealization of the input language of parser generators, we define a call-by-value calculus with first-order functions and a type-and-effect system where the effects are given by sequences of grammar symbols. The account of left-recursion elimination is then extended to this calculus.  相似文献   

9.
Plain CHOCS A second generation calculus for higher order processes   总被引:2,自引:0,他引:2  
  相似文献   

10.
We give a formal account of stream-based, service-centered calculus (SSCC), a calculus for modelling service-based systems, suitable to describe both service composition (orchestration) and the protocols that services follow when invoked (conversation). The calculus includes primitives for defining and invoking services, for isolating conversations (called sessions) among clients and servers, and for orchestrating services. The calculus is equipped with a reduction and a labelled transition semantics related by an equivalence result. SSCC provides a good trade-off between expressive power for modelling and simplicity for analysis. We assess the expressive power by modelling van der Aalst workflow patterns and an automotive case study from the European project Sensoria. For analysis, we present a simple type system ensuring compatibility of client and service protocols. We also study the behavioural theory of the calculus, highlighting some axioms that capture the behaviour of the different primitives. As a final application of the theory, we define and prove correct some program transformations. These allow to start modelling a system from a typical UML Sequence Diagram, and then transform the specification to match the service-oriented programming style, thus simplifying its implementation using web services technology.  相似文献   

11.
Verifying Programs with Unreliable Channels   总被引:1,自引:0,他引:1  
We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model, e.g., link protocols such as the Alternating Bit Protocol and HDLC. For this class of systems, we show that several interesting verification problems are decidable by giving algorithms for verifying (1) thereachability problem—is a finite set of global states reachable from some other global state of the system ? (2)safety properties over tracesformulated as regular sets of allowed finite traces, and (3)eventuality properties—do all computations of a system eventually reach a given set of states? We have used the algorithms to verify some idealized sliding-window protocols with reasonable time and space resources. Our results should be contrasted with the well-known fact that these problems are undecidable for systems with unboundedperfectFIFO channels.  相似文献   

12.
We introduce a semantics for classical logic with partial functions, in which ill-typed formulas are guaranteed to have no truth value, so that they cannot be used in any form of reasoning. The semantics makes it possible to mix reasoning about types and preconditions with reasoning about other properties. This makes it possible to deal with partial functions with preconditions of unlimited complexity. We show that, in spite of its increased complexity, the semantics is still a natural generalization of first-order logic with simple types. If one does not use the increased expressivity, the type system is not stronger than classical logic with simple types. We will define two sequent calculi for our semantics, and prove that they are sound and complete. The first calculus follows the semantics closely, and hence its completeness proof is fairly straightforward. The second calculus is further away from the semantics, but more suitable for practical use because it has better proof theoretic properties. Its completeness can be shown by proving that proofs from the first calculus can be translated.  相似文献   

13.
We investigate the addition of universal quantification to the meta-theory of Structural Operational Semantics (SOS). We study the syntax and semantics of SOS rules extended with universal quantification and propose a congruence rule format for strong bisimilarity that supports this new feature.  相似文献   

14.
This paper is concerned with transmission of Moving Picture Expert Group (MPEG) video over a Bluetooth wireless network using a fuzzy approach. MPEG Variable Bit Rate (VBR) video sources suffer from long delay and excessive loss due to the sudden bursts in bit rate. Constant Bit Rate (CBR) encoding scheme may work well for a network with a guaranteed bandwidth. However, a Bluetooth channel is subject to wireless interference and can never guarantee a constant bandwidth. Subsequently, it is impossible to transmit a CBR video over Bluetooth wireless without data loss or image quality degradation. To resolve this problem, a fuzzy control system is introduced at the Host Controller Interface (HCI). The system consists of a traffic-shaping buffer whose role is to prevent excessive back-to-back cells being generated during the peak transmissions of MPEG video sources. The output bit rate of the traffic-shaping buffer is controlled by a fuzzy controller to ensure that the video stream from the host conforms to the traffic condition of the Bluetooth channel. Another fuzzy controller regulates the average arrival bit rate to the traffic-shaper to guarantee that the buffer is neither full nor empty. Computer simulation results demonstrate that the use of the fuzzy controllers reduces excessive data loss at the HCI as compared with an open loop VBR/CBR video transmission in Bluetooth.  相似文献   

15.
16.
The applied pi calculus proposed by Abadi and Fournet is successful in the analysis of security protocols. Its semantics mainly depends on several structural rules. Structural rules are convenient for specification, but inefficient for implementation. In this paper, we establish a new semantics for applied pi calculus based upon pure labeled transition system and propose a new formulation of labeled bisimulation. We prove that the new labeled bisimularity coincides with observational equivalence. A zero-knowledge protocol is given as an example to illustrate the effectiveness of this new semantics.  相似文献   

17.
当前的Web服务尚没有充分的语义支持,无法支持动态的面向服务组合与协同.提出了智能Web服务的参考元模型,强化其语义支持的交互与推理能力,并仔细探讨了服务的内部结构及其实现.基于这一模型,开发了一套集成开发环境,并以此来验证模型的可行性.  相似文献   

18.
19.
Bonding calculus     
We present the bonding calculus, a calculus in which it is easy to handle covalent bonds between molecules. Our purpose is to use bonding calculus to model the dynamics of the interactions in biochemical systems. We provide an operational semantics by means of a transition system, and use a known software platform to both simulate the chemical reactions described naturally in bonding calculus and verify their specific properties.  相似文献   

20.
We present a method for efficiently providing algebraic correctness proofs for communication systems. It is described in the setting of μCRL [J.F. Groote, A. Ponse, The syntax and semantics of μCRL, in: A. Ponse, C. Verhoef, S.F.M. van Vlijmen (Eds.), Algebra of Communicating Processes, Workshops in Computing, Springer, Berlin, 1994, pp. 26–62] which is, roughly, ACP [J.C.M. Baeten, W.P. Weijland, Process Algebra, Cambridge Tracts in Theoretical Computer Science, vol. 18, Cambridge University Press, Cambridge 1990, J.A. Bergstra, J.W. Klop, The algebra of recursively defined processes and the algebra of regular processes, in: Proceedings of the 11th ICALP, Antwerp, Lecture Notes in Computer Science, vol. 172, Springer, Berlin, 1984, pp. 82–95] extended with a formal treatment of the interaction between data and processes. The method incorporates assertional methods, such as invariants and simulations, in an algebraic framework, and centers around the idea that the state spaces of distributed systems are structured as a number of cones with focus points. As a result, it reduces a large part of algebraic protocol verification to the checking of a number of elementary facts concerning data parameters occurring in implementation and specification. The resulting method has been applied to various non-trivial case studies of which a number have been verified mechanically with the theorem checker PVS. In this paper the strategy is illustrated by several small examples and one larger example, the Concurrent Alternating Bit Protocol (CABP).  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号