1,721,076 research outputs found
Characterising Concurrent Tests Based on Message Sequence Chart Requirements
No full textMSC-s specifying system requirements can be used to generate test scripts in languages such as TTCN. In 1996 TTCN was extended in order to describe concurrent test scripts. We give a characterisation of which concurrent tests can be executed by parallel test components (PTC-s) acting in concert. We also characterise when the PTC-s give the correct test result verdict
Thatched Partial Orders
No full textA thatch is a type of partial ordering which is most naturally described as a geometric construction. The geometry of these constructions is outlined in this note. A wait-and-see concurrent process may include any number of sub-processes, each regarded as a separate thread of execution. However if at any point the process launches a collection of concurrent threads it must wait and see how they terminate before proceeding. Each sub-process may also launch further sub-processes, which are also subject to the wait and see restriction. A wait-and-see process can be regarded as a thatch. This note describes some interesting mathematical properties of thatching that are relevant to these concurrent processes
Inductive completion with retracts
No full textIn this paper we give countably infinitely many extensions of Huet and Hullot's inductive completion procedure. Also we try and throw some light on the problem of functions which are only partially defined by some set of rewrite rules. We also give a procedure which attempts to show that two derived F-algebras are isomorphic when both of the algebras are realised as retracts
Finite State Automata for Topological Sorting
No full textA specification of concurrent communicating processes represents a causal relationship of the events contained in the specification. It is very simple to model this as a finite partial order over the set of events when the specification contains no iteration (e.g. for an MSC with no loop constructs). When there is iteration it is far more complex to express the causal relationships between the events within a mathematical setting. This paper first explores, in section 2, how to describe all total extensions of a partial order as a finite state automaton (FSA). These total extensions represent the test scripts for a specification when there is no iteration. Then, in section 3 we extend these ideas to specifications which contain complex iterations. For MSC this means the inline loop construct. Section 3.2 describes the algorithm for characterising an iterative specification as a FSA
QoS Provisioning and Orchestrating Processes within an SOA
No full textPresentation at a satellite workshop to 7th International Conference on integrated Formal Methods. Presentation discussed synthesis of real-time performance models for black box processes. The behavioural models were defined as timed stochastic finite state machines. An implementation of these models in PRISM was demonstrated
Coordinating Distributed Requirements Conformance Tests
No full textMessage sequence charts (MSC) requirements specifications are often used to generate TTCN conformance tests for telecommunications protocols. There are difficulties with constructing concurrent TTCN test scripts from an MSC used to describe test purposes. In [4] they demonstrate that without any timing restrictions it is not possible to automatically construct a concurrent test script from an MSC. They do not discuss in their paper when it is meaningful to construct concurrent conformance tests from the MSC. In this paper we give a characterisation of when coordinating messages added to an MSC produce a faithful and sound concurrent test. These results can be implemented in order to automatically generate such tests directly from the MSC
The Carcinogenic Example
No full textThis paper will introduce a new model for Linear Logic, the IE model (I for Internal E for External). Intuitively the model assumes there is a global environment which is divided up into an internal resource and an external resource. Such an assumption makes for an elementary definition of linear negation. The model results in a fairly natural semantics for the multiplicative operators and the constants of Linear Logic. A particular example of the model is given which gives a proper technical account of the cigarette exampl
Method for describing phase transitions in a partially specified telecommunications system protocol
No full textThis invention describes how to translate phase transition requirements defined with a graphical notation such as MSC-s or UML sequence diagrams into a form of abstract implementation which is useful for analysing feature combinations. This leads to a methodology for detecting feature conflicts in a partially specified system
Expressiveness for Highly Nested Expressions in Linear Temporal Logic
No full textIn the case where one only uses the modalities always, sometime and next it is shown that nesting modalities do not constrain a model in the limit any more than a non-nested formula. It is also proved that when the until modality operator is included then nesting modalities does constrain the limit of a model more than any non-nested formula
Modal Logic and Equality for Process Algebra
No full textThis paper provides a denotational semantics for the ‘saturation method’, described by J. A. Bergstra and J. W. Klop, in the form of a modal logic. In particular the semantics describes congruence for CCS processes in the form of a modal logic whose axioms are a modal representation of the tau laws. The main idea of the paper is to represent bisimulation equivalences of CCS in terms of a simple modal logic K. This logic is a variant of the classical modal logic K introducing a plus operator to mirror the choice operator of CCS. Weak bisimulation equivalence and process equality can be characterized in terms of extra axioms added to K. In the case of equality the axioms are a modal representation of the tau laws. A CCS process maps to a model of the logic; two processes are equivalent if they map to the same model
- …
