uu.seUppsala universitets publikationer
Ändra sökning
Avgränsa sökresultatet
1 - 38 av 38
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Träffar per sida
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
Markera
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 1.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Annichini, A
    Bouajjani, A
    Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol1999Ingår i: Tools and Algorithms for the Construction and Analysis of Systems: Proceddings of TACAS'99 / [ed] W. Rance Cleaveland, 1999, Vol. 1579, s. 208-222Konferensbidrag (Refereegranskat)
    Abstract [en]

    We consider the problem of verifying automatically infinite- state systems that are systems of finite machines that communicate by exchanging messages through unbounded lossy fifo channels. In a previous work [1], we proposed an algorithmic approach based on constructing a symbolic representation of the set of reachable configurations of a system by means of a class of regular expressions (SREs). The construction of such a representation consists of an iterative computation with an acceleration technique which enhances the chance of convergence. This technique is based on the analysis of the effect of iterating control loops. In the work we present here, we experiment our approach and show how it can be effectively applied. For that, we developed a tool prototype based on the results in [1]. Using this tool, we provide an automatic verification of (the parameterized version of) the Bounded Retransmission Protocol.

  • 2.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Bouajjani, A
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    On-the-fly analysis of systems with unbounded, lossy FIFO channels1998Ingår i: Computer Aided Verification: Proceedings of 10th International Conference, CAV'98 / [ed] Alan J. Hu, Moshe Y. Vardi, 1998, Vol. 1427, s. 305-318Konferensbidrag (Refereegranskat)
    Abstract [en]

    We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for (i) computing inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop of a program. All these operations are rather simple and can be carried out in polynomial time. With these techniques, one can construct a semi-algorithm which explores the set of reachable states of a protocol, in order to check various safety properties.

  • 3.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Cerans, K
    Simulation is decidable for one-counter nets1998Ingår i: CONCUR'98 Concurrency Theory: Proceedings of the 9th International Conference, 1998, Vol. 1466, s. 253-268Konferensbidrag (Refereegranskat)
    Abstract [en]

    We prove that the simulation preorder is decidable for the class of one-counter nets. A one-counter net consists of a finite-state machine operating on a variable (counter) which ranges over the natural numbers. Each transition can increase or decrease the value of the counter. A transition may not be performed if this implies that the value of the counter becomes negative. The class of one-counter nets is computationally equivalent to the class of Petri nets with one unbounded place, and to the class of pushdown automata where the stack alphabet is restricted to one symbol. To our knowledge, this is the first result in the literature which gives a positive answer to the decidability of simulation preorder between pairs of processes in a class whose elements are neither finite-state nor allow finite partitioning of their state spaces.

  • 4.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Undecidable verification problems for programs with unreliable channels1996Ingår i: Automata, Languages and Programming: Proceedings of ICALP 94 / [ed] Serge Abiteboul, Eli Shamir, 1996, Vol. 130, nr 1, s. 71-90Konferensbidrag (Refereegranskat)
    Abstract [en]

    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. In an earlier paper, we showed that several interesting verification problems are decidable for this class of systems, namely (1) the reachability problem: is a set of states reachable from some other state of the system, (2) safety property over traces formulated as regular sets of allowed finite traces, and (3) eventuality properties: do all computations of a system eventually reach a given set of states. In this paper, we show that the following problems are undecidable, namely

    • The model checking problem in propositional temporal logics such as Propositional Linear Time Logic (PTL) and Computation Tree Logic (CTL).

    • The problem of deciding eventuality properties with fair channels: do all computations eventually reach a given set of states if the unreliable channels are fair in the sense that they deliver infinitely many messages if infinitely many messages are transmitted. This problem can model the question of whether a link protocol, such as HDLC, will eventually reliably transfer messages across a medium that is not permanently broken.

    The results are obtained through a reduction from a variant of Post's Correspondence Problem.

  • 5.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Verifying networks of timed processes1998Ingår i: Tools and Algorithms for the Construction and Analysis of Systems: Proceedings of the 4th International Conference, TACAS'98 / [ed] Bernhard Steffen, 1998, Vol. 1384, s. 298-312Konferensbidrag (Refereegranskat)
    Abstract [en]

    Over the last years there has been an increasing research effort directed towards the automatic verification of infinite state systems, such as timed automata, hybrid automata, data-independent systems, relational automata, Petri nets, and lossy channel systems. We present a method for deciding reachability properties of networks of timed processes. Such a network consists of an arbitrary set of identical timed automata, each with a single real-valued clock. Using a standard reduction from safety properties to reachability properties, we can use our algorithm to decide general safety properties of timed networks. To our knowledge, this is the first decidability result concerning verification of systems that are infinite-state in “two dimensions”: they contain an arbitrary set of (identical) processes, and they use infinite data-structures, viz. real-valued clocks. We illustrate our method by showing how it can be used to automatically verify Fischer's protocol, a timer-based protocol for enforcing mutual exclusion among an arbitrary number of processes.

  • 6.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Kindahl, Mats
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Peled, D
    A general approach to partial order reductions in symbolic verification1998Ingår i: Computer Aided Verification: Proceedings of CAV'98 / [ed] Alan J. Hu, Moshe Y. Vardi, 1998, Vol. 1427, s. 379-390Konferensbidrag (Refereegranskat)
    Abstract [en]

    The purpose of partial-order reduction techniques is to avoid exploring several interleavings of independent transitions when model checking the temporal properties of a concurrent system. The purpose of symbolic verification techniques is to perform basic manipulations on sets of states rather than on individual states. We present a general method for applying partial order reductions to improve symbolic verification. The method is equally applicable to the verification of finite-state and infinite-state systems. It considers methods that check safety properties, either by forward reachability analysis or by backward reachability analysis. We base the method on the concept of commutativity (in one direction) between predicate transformers. Since the commutativity relation is not necessarily symmetric, this generalizes those existing approaches to partial order verification which are based on a symmetric dependency relation.

    We show how our method can be applied to several models of infinite-state systems: systems communicating over unbounded lossy FIFO channels, and unsafe (infinite-state Petri Nets. We show by a simple example how partial order reduction can significantly speed up symbolic backward analysis of Petri Nets.

  • 7.
    Ahlgren, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Swedish Institute of Computer Science.
    Improving Computer Communication Performance by Reducing Memory Bandwidth Consumption1997Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
  • 8.
    Berglund, Anders
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Daniels, Mats
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Improving education quality: a full scale study1997Ingår i: ACM SIGCSE Bulletin, ISSN 0097-8418, Vol. 29, nr 1, s. 330-334Artikel i tidskrift (Refereegranskat)
  • 9.
    Björnfot, Lars
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Specification and Implementation of Distributed Real-Time Systems for Embedded Applications1996Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
  • 10. Cleaveland, Rance
    et al.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Steffen, Bernhard
    The Concurrency Workbench: A Semantics Based Tool for the Verification of Concurrent Systems1993Ingår i: ACM Transactions on Programming Languages and Systems, ISSN 0164-0925, E-ISSN 1558-4593, Vol. 15, nr 1, s. 36-72Artikel i tidskrift (Refereegranskat)
  • 11.
    Daniels, Mats
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Asyl/EFSM: a language for specification of protocols and computers1985Licentiatavhandling, sammanläggning (Övrigt vetenskapligt)
  • 12.
    Gällmo, Olle
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Learning issues in artificial neural networks for ATM traffic control1995Licentiatavhandling, sammanläggning (Övrigt vetenskapligt)
  • 13.
    Jonsson, Bengt
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Deciding Bisimulation Equivalences for a Class of Non-Finite-State Programs1993Ingår i: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 107, nr 2, s. 272-302Artikel i tidskrift (Refereegranskat)
  • 14.
    Kindahl, Mats
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Verification of Infinite-State Systems: Decision Problems and Efficient Algorithms1999Doktorsavhandling, monografi (Övrigt vetenskapligt)
    Abstract [en]

    This thesis presents methods for the verification of distributed systems with infinite state spaces. We consider several verification problems for lossy channel systems, a class of infinite-state systems consisting of finite-state machines that communicate over unbounded, but lossy, FIFO channels. We also combine partial order techniques with symbolic techniques to improve performance of verification algorithms for infinite state systems.

    We study several implementation relations between lossy channel systems and finite transition systems, and show decidability of the following problems: trace inclusion, trace equivalence, simulation preorder, bisimulation equivalence, weak bisimulation equivalence in both directions, and weak simulation preorder in one direction. We further show that weak simulation preorder in the other direction is undecidable.

    Partial order reduction techniques are utilised to avoid exploring multiple interleavings of independent transitions. Constraint systems are introduced as a symbolic technique to represent (possibly infinite) sets of states. We present general methods for the application of partial order techniques for the verification of constraint systems. The method described is used for checking safety properties using forward or backward reachability analysis. It is based on the use of a—not necessarily symmetric—commutativity relation between operations. In contrast with previously existing approaches to partial order verification, which are based on a symmetric relation on transitions, our method does not require the relation to be symmetric. Partial order verification methods for lossy channel systems and for unsafe (i.e., infinite-state) Petri nets are developed to demonstrate the applicability of this approach.

  • 15. Larsen, Kim Guldstrand
    et al.
    Pettersson, Paul
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Yi, Wang
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    UPPAAL in a nutshell1997Ingår i: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1385-4879, E-ISSN 1571-8115, Vol. 1, nr 1-2, s. 134-152Artikel i tidskrift (Refereegranskat)
  • 16. Milner, Robin
    et al.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Walker, David
    A Calculus of Mobile Processes - Part I1992Ingår i: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 100, nr 1, s. 1-40Artikel i tidskrift (Refereegranskat)
  • 17. Milner, Robin
    et al.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Walker, David
    A Calculus of Mobile Processes - Part II1992Ingår i: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 100, nr 1, s. 41-77Artikel i tidskrift (Refereegranskat)
  • 18. Milner, Robin
    et al.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Walker, David
    Modal Logics for Mobile Processes1993Ingår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 114, nr 1, s. 149-171Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    In process algebras, bisimulation equivalence is typically defined directly in terms of the operational rules of action; it also has an alternative characterization in terms of a simple modal logic (sometimes called Hennessy-Milner logic). This paper first defines two forms of bisimulation equivalence for the π-calculus, a process algebra which allows dynamic reconfiguration among processes; it then explores a family of possible logics, with different modal operators. It is proven that two of these logics characterize the two bisimulation equivalences. Also, the relative expressive power of all the logics is exhibited as a lattice. The results are applicable to most value-passing process algebras.

  • 19. Nestmann, Uwe
    et al.
    Victor, Björn
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Calculi for Mobile Processes: Bibliography and Web Pages1998Ingår i: Bulletin of the EATCS, Vol. 64Artikel, forskningsöversikt (Övrig (populärvetenskap, debatt, mm))
    Abstract [en]

    With this note we present a quick overview on the work that has been done to collect (online) resources - an extensive up-to-date bibliography and a web page for further information - covering the area of calculi for mobile processes. Therefore, we quickly recapitulate the history of this area from our point of view, which is witnessed by the number of respective research papers in the field.

  • 20.
    Nordström, Ernst
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Markov Decision Problems in ATM Traffic Control1998Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
    Abstract [en]

    This thesis discusses how to make cost-effective use of the communication resources in the Broadband Integrated Services Digital Network (B-ISDN), which is based on the Asynchronous Transfer Mode (ATM) switching and multiplexing technique.

    The thesis deals with two important functions in ATM traffic control, namely Call Admission Control (CAC) and routing, which affects both the network operator's revenue over time and the users' Quality of Service (QOS) and Grade of Service (GOS). The routing function finds a route, expressed in terms of successive links, with sufficient QOS (e.g. cell loss probability) according to the CACQOS function. The CACGOS function accepts or rejects the call request based on fairness (e.g. call blocking probability) and revenue considerations.

    The CACGOS and routing tasks are modelled a Semi-Markov Decision Problem (SMDP). The SMDP solution gives high resource utilization and ability to control GOS distribution between the call classes. In SMDP routing, the task is to control the state transitions between reward generating states such that the average reward rate is maximized. In order to obtain a solution with feasible computational complexity, the network SMDP is decomposed into a set of link SMDPs. Each link SMDP is solved by either dynamic programming (DP) or reinforcement learning (RL). DP is based on a model of the decision task in terms of the state transition probabilities and expected reward in each state. RL is not based on a model of the decision task. Instead, the optimal policy is found from simulated state transitions, where long-term reward predictions are corrected by temporal difference learning.

    We study aspects such as delayed set up of wide-band calls, link-level integration of guaranteed QOS services and best effort services, and Poisson versus self-similar call arrival processes.

  • 21. Orava, Fredrik
    et al.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    An Algebraic Verification of a Mobile Network1992Ingår i: Formal Aspects of Computing, ISSN 0934-5043, E-ISSN 1433-299X, Vol. 4, nr 6, s. 497-543Artikel i tidskrift (Refereegranskat)
  • 22.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Interaction Diagrams1995Ingår i: Nordic Journal of Computing, ISSN 1236-6064, Vol. 2, nr 4, s. 407-443Artikel i tidskrift (Refereegranskat)
  • 23.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Programmeraren som Schaman1998Ingår i: Forskning och Framsteg, ISSN 0015-7937, nr 2, s. 14-19Artikel i tidskrift (Övrig (populärvetenskap, debatt, mm))
  • 24.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Structural and Behavioural Equivalences of Networks1993Ingår i: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 107, nr 1, s. 58-90Artikel i tidskrift (Refereegranskat)
  • 25.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Submodule Construction as Equation Solving in CCS1989Ingår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 68, nr 2, s. 175-202Artikel i tidskrift (Refereegranskat)
  • 26.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    The Expressive Power of Parallelism1990Ingår i: Future generations computer systems, ISSN 0167-739X, E-ISSN 1872-7115, Vol. 6, nr 3, s. 271-285Artikel i tidskrift (Refereegranskat)
  • 27.
    Parrow, Joachim
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sangiorgi, Davide
    Algebraic Theories of Name-Passing Calculi1995Ingår i: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 120, nr 2, s. 174-197Artikel i tidskrift (Refereegranskat)
  • 28.
    Parrow, Joachim
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sjödin, Peter
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Designing a Multiway Synchronisation Protocol1996Ingår i: Computer Communications, ISSN 0140-3664, E-ISSN 1873-703X, Vol. 19, nr 14, s. 1151-1160Artikel i tidskrift (Refereegranskat)
  • 29.
    Parrow, Joachim
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sjödin, Peter
    Multiway Synchronization Verified with Coupled Simulation1992Ingår i: Proceedings of CONCUR '92 / [ed] W.R. Cleaveland, Berlin: Springer , 1992, s. 518-533Konferensbidrag (Refereegranskat)
    Abstract [en]

    We consider the problem of implementing multiway synchronization in a distributed environment providing only binary asynchronous communication. Our implementation strategy is formulated as a transformation on transition systems and we give a distributed algorithm for multiway synchronization. Correctness assertions and proofs are based on a new method: coupled simulations. The coupled simulation equivalence is weaker than observation equivalence and stronger than testing equivalence and combines some of their advantages. Like observation equivalence (and unlike testing) it is established through case analysis over single transitions. Like testing equivalence (and unlike observation) it allows an internal choice to be distributed onto several internal choices. The latter is particularly important when relating our distributed implementations to their specifications.

  • 30.
    Parrow, Joachim
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Sjödin, Peter
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    The Complete Axiomatization of Cs-Congruence1994Ingår i: Proceedings of STACS 94 / [ed] Patrice Enjalbert, Ernst W. Mayr, Klaus W. Wagner, Berlin: Springer , 1994, s. 557-568Konferensbidrag (Refereegranskat)
    Abstract [en]

    The coupled simulation equivalence is slightly larger than observation equivalence. Where observation equivalence is based on weak bisimulations, coupled simulation equivalence is based on pairs of simulations which coincide at stable states. We establish the corresponding congruence and provide a complete axiomatization by adding a new -law, .(. P + Q) = . P + Q, to the axiomatization of observation congruence. We further indicate how the definition of the equivalence can be extended to divergent transition systems.

  • 31.
    Parrow, Joachim
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Victor, Björn
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes1998Ingår i: Proceedings of LICS'98, Los Alamitos, CA: IEEE Computer Society, 1998, s. 176-185Konferensbidrag (Refereegranskat)
    Abstract [en]

    We present the fusion calculus as a significant step towards a canonical calculus of concurrency. It simplifies and extends the pi-calculus.

    The fusion calculus contains the polyadic pi-calculus as a proper subcalculus and thus inherits all its expressive power. The gain is that fusion contains actions akin to updating a shared state, and a scoping construct for bounding their effects. Therefore it is easier to represent computational models such as concurrent constraints formalisms. It is also easy to represent the so called strong reduction strategies in the lambda-calculus, involving reduction under abstraction. In the pi-calculus these tasks require elaborate encodings.

    The dramatic main point of this paper is that we achieve these improvements by simplifying the pi-calculus rather than adding features to it. The fusion calculus has only one binding operator where the pi-calculus has two (input and restriction). It has a complete symmetry between input and output actions where the pi-calculus has not. There is only one sensible variety of bisimulation congruence where the pi-calculus has at least three (early, late and open). Proofs about the fusion calculus, for example in complete axiomatizations and full abstraction, therefore are shorter and clearer.

    Our results on the fusion calculus in this paper are the following. We give a structured operational semantics in the traditional style. The novelty lies in a new kind of action, fusion actions for emulating updates of a shared state. We prove that the calculus contains the pi-calculus as a subcalculus. We define and motivate the bisimulation equivalence and prove a simple characterization of its induced congruence, which is given two versions of a complete axiomatization for finite terms. The expressive power of the calculus is demonstrated by giving a straight-forward encoding of the strong lazy lambda-calculus, which admits reduction under lambda abstraction.

  • 32.
    Parrow, Joachim
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Victor, Björn
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    The Tau-Laws of Fusion1998Ingår i: Proceedings of CONCUR'98 / [ed] Davide Sangiorgi, Robert de Simone, Berlin: Springer, 1998, s. 99-114Konferensbidrag (Refereegranskat)
    Abstract [en]

    We present complete axiomatizations of weak hypercongruence in the finite fragment of the fusion calculus, an extension and simplification of the pi-calculus. We treat both the full fusion calculus and the subcalculus without mismatch operators. The axiomatizations are obtained from the laws for hyperequivalence and adding so called tau-laws. These are similar to the well known tau-laws for CCS and the pi-calculus, but there is an interesting difference which highlights an aspect of the higher expressive power of the fusion calculus.

  • 33.
    Parrow, Joachim
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Victor, Björn
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    The Update Calculus1997Ingår i: Proceedings of AMAST'97 / [ed] Michael Johnson, Berlin: Springer , 1997, s. 409-423Konferensbidrag (Refereegranskat)
    Abstract [en]

    In the update calculus concurrent processes can perform update actions with side effects, and a scoping operator can be used to control the extent of the update. In this way it incorporates fundamental concepts both from imperative languages or concurrent constraints formalisms, and from functional formalisms such as the lambda- and pi-calculi. Structurally it is similar to but simpler than the pi-calculus; it has only one binding operator and a symmetry between input and output. We define the structured operational semantics and the proper bisimulation equivalence and congruence, and give a complete axiomatization. The pi-calculus turns out to be an asymmetric subcalculus.

  • 34.
    Pettersson, Paul
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice1999Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
    Abstract [en]

    During the last decade, model-checking techniques for the verification of timed system have been developed baaed on the theory of timed automata. The practical limitation in applying these techniques to industrial-size systems is the huge amount of time and memory needed to explore and store the state-space of the system model.

    In this thesis, we improve the current status of model-checking techniques for timed systems by developing symbolic, on-the-fly and compositional verification techniques for timed automata. A common characteristics of the model-checking techniques presented is that they use efficient constraint-solving techniques to symbolically represent and manipulate the state-space. To avoid construction of the full state-space of the system model two techniques are used: on-the-fly generation of the state-space and a compositional model-checking technique. The memory-usage is further reduced by developing a minimal and canonical data structure for the class of constraints used in the model-checking algorithm, which reduces the size of each individual state. Two other techniques to reduce the total number of states explored and stored during verification are also presented.

    The developed techniques have been implemented in the verification tool UPPAAL. To demonstrate the potential applications of our model-checking techniques, we present three industrial-size case studies where the UPPAAL tool is applied.

  • 35.
    Victor, Björn
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik.
    The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes1998Doktorsavhandling, monografi (Övrigt vetenskapligt)
    Abstract [en]

    The fusion calculus is presented as a significant step towards a canonical calculus of concurrency. It simplifies and extends the π-calculus of Milner, Parrow and Walker.

    The fusion calculus contains the polyadic π-calculus as a proper subcalculus and thus inherits all its expressive power. In addition fusion contains actions akin to updating a shared state, and a scoping construct for bounding their effects. Therefore it is easier to represent computational models with shared state, including concurrent constraint formalisms. It is also easy to represent the so called strong reduction strategies in the Λ-calculus, involving reduction under abstraction. In the π-calculus thesetasks require elaborate encodings.

    The fusion calculus simplifies the π-calculus by reducing the number of binding operators and the number of bisimulation equivalences, and by making input and output symmetric like in pure CCS. We attain a calculus where concepts from other models of computation are more easily expressed than in the π-calculus, thereby taking a step towards a unified yet simple model of computation.

    In this thesis we present a broad foundational theory of the fusion calculus. We define its labelled and unlabelled operational semantics, and treat strong and weak bisimulation equivalences for both semantics in some detail, including complete axiom systems for finite terms. The equivalences are given symbolic characterisations, leading to algorithms and an automatic tool for equivalence checking. We demonstrate the expressive power of the fusion calculus to give simple encodings of foundational calculi for functional and concurrent constraint programming.

  • 36.
    Victor, Björn
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Moller, Faron
    The Mobility Workbench: A Tool for the Pi-Calculus1994Ingår i: Proceedings of CAV'94, 1994, s. 428-440Konferensbidrag (Refereegranskat)
    Abstract [en]

    In this paper we describe the first prototype version of the Mobility Workbench (MWB), an automated tool for manipulating and analyzing mobile concurrent systems (those with evolving connectivity structures) described in the pi-calculus. The main feature of this version of the MWB is checking open bisimulation equivalences. We illustrate the MWB with an example automated analysis of a handover protocol for a mobile telephone system.

  • 37.
    Victor, Björn
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Concurrent Constraints in the Fusion Calculus1998Ingår i: Proceedings of ICALP'98 / [ed] Kim G. Larsen, Sven Skyum, Glynn Winskel, Berlin: Springer, 1998, s. 455-469Konferensbidrag (Refereegranskat)
    Abstract [en]

    We use the fusion calculus, a generalization and simplification of the pi-calculus, to model concurrent constraint programming. In particular we encode three basic variants of the rho-calculus, which is a foundational calculus for the concurrent constraint programming language Oz. Using a new reduction-based semantics and weak barbed congruences for the fusion calculus we formally establish an operational correspondence between the rho-calculi and their encodings. These barbed congruences are shown to coincide with the hyperequivalences previously adopted for the fusion calculus.

  • 38.
    Victor, Björn
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Parrow, Joachim
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Constraints as Processes1996Ingår i: Proceedings of CONCUR'96 / [ed] Ugo Montanari, Vladimiro Sassone, Berlin: Springer , 1996, s. 389-405Konferensbidrag (Refereegranskat)
    Abstract [en]

    We present a compositional encoding of the gamma-calculus into the pi-calculus. The former, used in the Oz semantics, is a recent small language with equational constraints over logical variables; the latter is a basic calculus of interacting processes. We establish a close correspondence between the reductions in the gamma-calculus and its encoding, using weak barbed bisimulation congruence.

1 - 38 av 38
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf