Publications

2012

2011

2010

  • Quantitative Analysis of Weighted Transition Systems by Claus Thrane, Uli Fahrenberg, Kim Guldstrand Larsen, Journal of Logic and Algebraic Programming vol: 79 pages: 689-703, 2010PDF, BibTex, Show Abstract.
    We present a general framework for the analysis of quantitative and qualitative properties of reactive systems, based on a notion of weighted transition systems. We introduce and analyze three different types of distances on weighted transi- tion systems, both in a linear and a branching version. Our quantitative notions appear to be reasonable extensions of the standard qualitative concepts, and the three different types introduced are shown to measure inequivalent properties. When applied to the formalism of weighted timed automata, we show that some standard decidability and undecidability results for timed automata extend to our quantitative setting.
  • Timed I/O automata: a complete specification theory for real-time systems by Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Andrzej Wasowski, in Proceedings of the 13th ACM International Conference on Hybrid Systems: Computa tion and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010 (HSCC) Editor: Karl Henrik Johansson and Wang YiACM ACM Proceedings of the 13th ACM International Conference on Hybrid Systems: Computa tion and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010 (HSCC) Editor: Karl Henrik Johansson and Wang YiACM ACM , pages: 91-100, 2010EE, BibTex, Show Abstract.
    A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation and a set of operators supporting stepwise design. We develop a complete specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications---all indispensable ingredients of a compositional design methodology. The theory is implemented on top of an engine for timed games, tiga, and illustrated with a small case study.
  • Timed automata with observers under energy constraints by Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, in Proceedings of the 13th ACM International Conference on Hybrid Systems: Computa tion and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010 (HSCC) Editor: Karl Henrik Johansson and Wang YiACM ACM Proceedings of the 13th ACM International Conference on Hybrid Systems: Computa tion and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010 (HSCC) Editor: Karl Henrik Johansson and Wang YiACM ACM , pages: 61-70, 2010EE, BibTex, Show Abstract.
    In this paper, we study one-clock priced timed automata in which prices can grow linearly or exponentially, with discontinuous updates on edges. We propose EXPTIME algorithms to decide the existence of controllers that ensure existence of infinite runs (or reachability of some goal location) with non-negative observer value all along the run. These algorithms consist in computing the optimal delays that should be elapsed in each location along a run, so that the final observer value is maximized (and never goes below zero).
  • Scenario-based analysis and synthesis of real-time systems using uppaal by Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, Saulius Pusinskas, in DATE: Design, Automation and Test in Europe, DATE 2010, Dresden, Germany, March 8-12, pages: 447-452, 2010EE, BibTex, Show Abstract.
    We propose an automated, tool-supported approach to scenario-based analysis and synthesis of real-time embedded systems. The inter-object behaviors of a system are modeled as a set of live sequence charts (LSCs), and the scenario-based user requirement is specified as a separate LSC. By translating the set of LSC charts into a behavior-equivalent network of med automata (TA), we reduce the problems of model consistency checking and property verification to classical CTL real-time model checking problems, and reduce the problem of centralized synthesis for open systems to a timed game solving problem. We implement a prototype LSC-to-TA translator, which can be linked to exisisting real-time model checker UPPAAL and timed game solver UPPAALTIGA. Preliminary experiments on a number of examples show that it is a viable approach.
  • METAMOC: Modular Execution Tiem Analysis using Model Checking by Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, Rene R. Hansen, Kim G. Larsen, in Proceedings of 10th International Workshop on Worst-Case Execution Time Analysis, 2010 (To appear.), BibTex, Show Abstract.
    Safe and tight worst-case execution times (WCETs) are important when scheduling hard real-time systems. This paper presents METAMOC, a path-based, modular method, based on model checking and stastic analysis, that determines safe and tight WCETs for programs running on platforms featuring caching and pipelining. The method works by constructing a UPPAAL model of the program being analysed and annotating the model with information from an inter-procedural value analysis. The program model is then combined with a model of the hardware platform, and model checked for the WCET. Through support for the platforms ARM7, ARM9 and ATMEL AVR 8-bit the modularity and retargetability of the method is demonstrated, as only the pipeline needs to be remodelled. Modelling the hardware is performed in a state-ofthe- art graphical modeling environment. Experiments on the Malardalen WCET benchmark programs show that taking caching into account yields much a tighter WCETs, and that METAMOC is a fast and versatile approach for WCET analysis.
  • Compositional Design Methodology with Constraint Markov Chains by Benoit Caillaud, Benoit Delahaye, Kim G. Larsen, Axel Legay, Mikkel Larsen Pedersen, Andrzej Wasowski, in Proceedings of 7th International Conference on Quantitative Evaluation of SysTems (QEST), 2010 (To appear), BibTex, Show Abstract.
    Notions of specification, implementation, satisfaction, and refinement, together with operators supporting stepwise design, constutes a specification theory. We construct such a theory for Markov Chains (MCs) employing a new abstraction of a Constraint MC. Constraint MCs permit rich constraints on probability distributions and thus generalize prior abstractions such as Interval MCs. Linear (polynomial) constraints suffice for closure under conjunction (respectively parallel composition). This is the first specification theory for MCs with such closure properties. We discuss its relation to simpler operators for known languages such as probabilistic process algebra. Despite the generality, all operators and relations are computable.
  • ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems by Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Andrzej Wasowski, in Proceedings of 8th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2010 (To appear), BibTex, Show Abstract.
    We present Ecdar a new tool for compositional design and verification of real time systems. In Ecdar, a component interface describes both the behavior of the component and the components assumptions about the environment. The tool supports the important operations of a good compositional reasoning theory: composition, conjunction, quotient, consistency/satisfaction checking, and refinement. The operators can be used to combine basic models into larger specifications to construct comprehensive system descriptions from basic requirements. Algorithms to perform these operations have been based on a game theoretical setting that permits, for example, to capture the real-time constraints on communication events between components. The compositional approach allows for scalability in the verification.
  • Developing UPPAAL over 15 Years by Gerd Behrmann, Alexandere David, Kim G. Larsen, Paul Pettersson, Wang Yi, Software - Practice and Experience 2010 (To appear), BibTex, Show Abstract.
    Uppaal is a tool suitable for model checking real-time systems described as networks of timed automata communicating by channel synchronisations and extended with integer variables. Its first version was released in 1995 and its development is still very active. It now features an advanced modelling language, a user-friendly graphical interface, and a performant model checker engine. In addition, several flavours of the tool have matured in recent years. In this paper, we present how we managed to maintain the tool during 15 years, its current architecture with its challenges, and we give future directions of the tool.
  • An Interface Theory for Timed Systems by Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Andrzej Wasowski, in Proceedings of 20th International Workshop on Algebraic Development Techniques WADT, 2010 (To appear), BibTex, Show Abstract.
    We propose to survey our new theory for compositional design and verification of real time systems. In our theory, a component interface describes both the behavior of the component and the components assumptions about the environment. The theory supports the important operations of a good compositional reasoning theory: composition, conjunction, quotient, consistency/satisfaction checking, and refinement. The operators can be used to combine basic models into larger specifications to construct comprehensive system descriptions from basic requirements. Algorithms to perform these operations have been based on a game theoretical setting that permits, for example, to capture the real-time constraints on communication events between components. The compositional approach allows for scalability in the verification. The theory has been implemented in a tool that will also be presented.
  • Present and Absent Sets: Abstraction for Testing of Reactive Systems with Databases by Petur Olsen, Kim G. Larsen, Arne Skou, in Proceedings of 6th Workshop on Model-Based Testing, 2010BibTex, Show Abstract.
    We present a new abstraction of reactive systems interacting with databases. This abstraction is intended to be used for model-based testing. We abstract the database into two sets: present set and absent set, and present a proof of this abstrac- tion. We present two extensions of FSM, the DBFSM and PAFSM. DBFSM are a form of FSM incorporating databases. PAFSM are an abstraction of DBFSM using present-absent sets. Depending on what type of testing is to be done, the translation is tailored to fit this purpose. We show how this translation is related to the present-absent abstraction. Finally, we illustrate the approach through a small example and show how this can be used for testing with the model-based testing tool Uppaal TRON.
  • A Quantitatve Characterization of Weighted Kripke Structures in Temporal Logic by Uli Fahrenberg, Kim G. Larsen, Claus Thrane, Journal of Computing and Informatics 2010 (to appear), BibTex, Show Abstract.
    We extend the usual notion of Kripke structures with a weighted transition relation and generalize the classical Boolean interpretation of CTL to a map which assigns to states and temporal formulae a real-valued distance describing the degree of satisfaction. We describe a general approach to obtaining quantitative interpretations for a generic extension of the CTL syntax and show that, for one such interpretation, the logic is both adequate and expressive with respect to quantitative bisimulation.
  • Symbolic and Compositional Reachability for Timed Automata by Kim Guldstrand Larsen, in Reachability Problems, 4th International Workshop, RP 2010, Brno, Czech Republic, August 28-29, 2010. Proceedings (RP) Editor: Antonin Kucera and Igor Potapov of Lecture Notes in Computer Science, vol: 6227 ©Springer-Verlag, pages: 24-28, 2010EE, BibTex, Show Abstract.
    The model-checker UPPAAL is based on the theory of timed automata and its modeling languague offers additional features such as networks of timed automata, clocks and stop-watches, synchronizing over synchronous and broadcast channels, discrete variables ranging over bounded integers or structured types (arrays and records) as well as user-defined types and functions. In the following we give an overview of the development of the datastuctures and algorithms underlying the verification engines of UPPAAL and CORA as well as indicate on-going research directions.
  • Schedulability Analysis Using Uppaal: Herscehl-Planck Case Study by M. Mikucionis, K.G. Larsen, B. Nielsen, J. Illum, A. Skou, S.U. Palm, J.S. Pedersen, P. Hougaard, in Proceedings of 4th International Symposiumo on Leveraging Applications of Formal Methods, Verification and Validation; track: Quantitative Verification in Practice, 2010BibTex, Show Abstract.
    We propose a modeling framework for performing schedulability analysis by using Uppaal real-time model-checker. The frame-work is inspired by a case study where schedulability analysis of a satellite system is performed. The framework assumes a single CPU hardware where a fixed priority preemptive scheduler is used in a combination with two resource sharing protocols and in addition voluntary task suspension is considered. The contributions include the modeling framework, its application on an industrial case study and a comparison of results with classical response time analysis.
  • On Zone-Based Analysis of Duration Probabilistic Automata by O. Maler, K.G. Larsen, B. Krogh, in Proceedings of INFINITY, International Workshop on Verification of Infinite-State Systems, 2010BibTex, Show Abstract.
    We propose an extension of the zone-based algorithmics for analyzing timed automata to handle systems where timing uncertainty is considered as probabilistic rather than set-theoretic. We study duration probabilistic automata (DPA), expressing multiple parallel processes admitting memoryfull continuouslydistributed durations. For this model we develop an extension of the zone-based forward reachability algorithm whose successor operator is a density transformer, thus providing a solution to verification and performance evaluation problems concerning acyclic DPA (or the bounded-horizon behavior of cyclic DPA).
  • Modal and mixed specifications: key decision problems and their complexities by Adam Antonik, Michael Huth, Kim G. Larsen, Ulrik Nyman, Andrzej Wasowski, Mathematical Structures in Computer Science vol: 20 pages: 75-103, 2010BibTex, Show Abstract.
    Modal and mixed transition systems are specification formalisms that allow the mixing of over- and under-approximation. We discuss three fundamental decision problems for such specifications: 1) whether a set of specifications has a common implementation; 2) whether an individual specification has an implementation; and 3) whether all implementations of an individual specification are implementations of another one. For each of these decision problems we investigate the worst-case computational complexity for the modal and mixed cases. We show that the first decision problem is EXPTIME-complete for both modal and mixed specifications. We prove that the second decision problem is EXPTIME-complete for mixed specifications (it is known to be trivial for modal ones). The third decision problem is also shown to be EXPTIME-complete for mixed specifications.

2009

  • EXPTIME-complete Decision Problems for Modal and Mixed Specifications by Adam Antonik, Michael Huth, Kim Guldstrand Larsen, Ulrik Nyman, Andrzej Wasowski, Electr. Notes Theor. Comput. Sci. vol: 242 pages: 19-33, 2009EE, PDF, BibTex,
  • Discount-Optimal Infinite Runs in Priced Timed Automata by Ulrich Fahrenberg, Kim Guldstrand Larsen, Electr. Notes Theor. Comput. Sci. vol: 239 pages: 179-191, 2009EE, PDF, BibTex,
  • Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete by Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, Jiri Srba, in Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings (ICTAC) Editor: Martin Leucker and Carroll Morgan of Lecture Notes in Computer Science, vol: 5684 ©Springer-Verlag, pages: 112-126, 2009EE, PDF, BibTex,
  • Automatic Synthesis of Robust and Optimal Controllers - An Industrial Case Study by Franck Cassez, Jan Jakob Jessen, Kim Guldstrand Larsen, Jean-Franccois Raskin, Pierre-Alain Reynier, in Hybrid Systems: Computation and Control, 12th International Conference, HSCC 2009, San Francisco, CA, USA, April 13-15, 2009. Proceedings (HSCC) Editor: Rupak Majumdar and Paulo Tabuada of Lecture Notes in Computer Science, vol: 5469 ©Springer-Verlag, pages: 90-104, 2009EE, PDF, BibTex,
  • Verification, Performance Analysis and Controller Synthesis for Real-Time Systems by Uli Fahrenberg, Kim Guldstrand Larsen, Claus Thrane, in Proceedings of 3rd International Conference on Fundamentals of Software Engineering, 15 - 17 April, Kish Island, Persian Gulf, Iran (FSEN 09) ©Springer-Verlag, 2009 (to appear), BibTex, Show Abstract.
    This note aims at providing a concise and precise Travellers Guide, Phrase Book or Reference Manual to the timed automata mod- eling formalism introduced by Alur and Dill [7,8]. The note gives com- prehensive definitions of timed automata, priced (or weighted) timed automata, and timed games and highlights a number of results on asso- ciated decision problems related to model checking, equivalence checking, optimal scheduling, and winning strategies
  • Quantitative Modeling and Analysis of Embedded Systems by Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Communications of the ACM 2009 (Invited paper, to appear), BibTex,
  • On Determinism in Modal Transition Systems by Nikola Benes, Jan Kretinsky, Kim Guldstrand Larsen, Jiri Srba, Special Issue of Theoretical Computer Science 2009 (to appear), BibTex,
  • UPPAAL TIGA 2009 - towards realizable strategies by Alexandre David, Kim Guldstrand Larsen, Didier Lime, in Proceedings of Workshop on Games for Design, Verification and Synthesis, GASICS, 2009 (to appear), BibTex,
  • Quantitative and Compositional Model Checking by Kim Guldstrand Larsen, in Proceedings of Seventh International Andrei Ershov Memorial Conference (PSI), Novosibirsk, Russia, 2009 (to appear), BibTex,
  • Quantitative Verification and Validation of Embedded Systems by Kim Guldstrand Larsen, in Proceedings of of 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE09, Tianjin, China, 2009 (to appear), BibTex,
  • Discounting in Time by Ulrich Fahrenberg, Kim Guldstrand Larsen, in proceedings of 7th Workshop on Quantitative Aspects of Programming Languages, 2009 (to appear), BibTex,
  • Timed Testing under Partial Observability by Alexandre David, Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, Software Testing, Verification, and Validation, 2008 International Conference on vol: 0 IEEE Computer Society pages: 61-70, 2009EE, BibTex, Show Abstract.
    This paper studies the problem of model-based testing of real-time systems that are only partially observable. We model the System Under Test (SUT) using Timed Game Automata (TGA) which has internal actions, uncontrollable outputs and timing uncertainty of outputs. We define the partial observability of SUT using a set of predicates over the TGA state space, and specify the test purposes in Computation Tree Logic (CTL) formulas. A recently developed partially observable timed game solver is used to generate winning strategies, which are used as test cases. We propose a conformance testing framework, define a partial observation-based conformance relation, present the test execution algorithms, and prove the soundness and completeness of this test method (i.e., a detected error really violates the conformance relation; and if the SUT violates the test purpose, then a test case can be generated to detect this violation). Experiments on some non-trivial examples show that this method yields encouraging results.
  • UPPAAL PRO: Tool for Performance Analysis of Probabilistic Timed Automata by Alexandre David, Arild Haugstad, Kim G. Larsen, 2009 (Under submission), BibTex,
  • Teaching Concurrency: Theory in Practice by Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen, Jiri Srba, 2009 (Under submission), BibTex,
  • Verifying Real-Time Systems against Scenario-Based Requirements by Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, Saulius Pusinskas, in FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings (FM) Editor: Ana Cavalcanti and Dennis Dams of Lecture Notes in Computer Science, vol: 5850 ©Springer-Verlag, pages: 676-691, 2009EE, PDF, BibTex, Show Abstract.
    We propose an approach to automatic verification of realtime systems against scenario-based requirements. A real-time system is modeled as a network of Timed Automata (TA), and a scenario-based requirement is specified as a Live Sequence Chart (LSC). We define a trace-based semantics for a kernel subset of the LSC language. By equivalently translating an LSC chart into an observer TA and then nonintrusively composing this observer with the original system model, the problem of verifying a real-time system against a scenario-based requirement reduces to a classical real-time model checking problem. We show how this is accomplished in the context of the Uppaal model checker.
  • A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic by Uli Fahrenberg, Kim G. Larsen, Claus Thrane, in Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMIC09), 2009 (Best paper award), BibTex,

2008

  • Optimal reachability for multi-priced timed automata by Kim Guldstrand Larsen, Jacob Illum Rasmussen, Theor. Comput. Sci. vol: 390 pages: 197-213, 2008EE, PDF, BibTex,
  • Model Checking One-Clock Priced Timed Automata by Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, Logical Methods in Computer Science vol: 4 2008EE, BibTex,
  • Optimal infinite scheduling for multi-priced timed automata by Patricia Bouyer, Ed Brinksma, Kim Guldstrand Larsen, Formal Methods in System Design vol: 32 pages: 3-23, 2008EE, PDF, BibTex, Show Abstract.
    This paper is concerned with the derivation of infinite schedules for timed automata that are in some sense optimal. To cover a wide class of optimality criteria we start out by introducing an extension of the (priced) timed automata model that includes both costs and rewards as separate modelling features. A precise definition is then given of what constitutes optimal infinite behaviours for this class of models. We subsequently show that the derivation of optimal non-terminating schedules for such double-priced timed automata is computable. This is done by a reduction of the problem to the determination of optimal mean-cycles in finite graphs with weighted edges. This reduction is obtained by introducing the so-called corner-point abstraction, a powerful abstraction technique of which we show that it preserves optimal schedules.
  • Cooperative Testing of Timed Systems by Alexandre David, Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, Electr. Notes Theor. Comput. Sci. vol: 220 pages: 79-92, 2008EE, PDF, BibTex,
  • Model Checking One-clock Priced Timed Automata by Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, CoRR vol: abs/0805.1457 2008EE, BibTex,
  • Fast Directed Model Checking Via Russian Doll Abstraction by Sebastian Kupferschmid, Jörg Hoffmann, Kim Guldstrand Larsen, in Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (TACAS) Editor: C. R. Ramakrishnan and Jakob Rehof of Lecture Notes in Computer Science, vol: 4963 ©Springer-Verlag, pages: 203-217, 2008EE, PDF, BibTex,
  • Model-based schedulability analysis of safety critical hard real-time Java programs by Thomas Bøgholm, Henrik Kragh-Hansen, Petur Olsen, Bent Thomsen, Kim Guldstrand Larsen, in Proceedings of the 6th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES 2008, 24-26 September 2008, Santa Clara, California, USA (JTRES) Editor: Gregory Bollella and C. Douglas Locke of ACM International Conference Proceeding Series, vol: 343 ACM , pages: 106-114, 2008EE, PDF, BibTex,
  • Testing Real-Time Systems Using UPPAAL by Anders Hessel, Kim Guldstrand Larsen, Marius Mikucionis, Brian Nielsen, Paul Pettersson, Arne Skou, in Formal Methods and Testing, An Outcome of the FORTEST Network, Revised Selected Papers (Formal Methods and Testing) Editor: Robert M. Hierons and Jonathan P. Bowen and Mark Harman of Lecture Notes in Computer Science, vol: 4949 ©Springer-Verlag, pages: 77-117, 2008EE, PDF, BibTex, Show Abstract.
    This chapter presents principles and techniques for model-based black-box conformance testing of real-time systems using the Uppaal model-checking tool-suite. The basis for testing is given as a network of concurrent timed automata specified by the test engineer. Relativized input/output conformance serves as the notion of implementation correctness, essentially timed trace inclusion taking environment assumptions into account. Test cases can be generated offline and later executed, or they can be generated and executed online. For both approaches this chapter discusses how to specify test objectives, derive test sequences, apply these to the system under test, and assign a verdict.
  • Complexity of Decision Problems for Mixed and Modal Specifications by Adam Antonik, Michael Huth, Kim Guldstrand Larsen, Ulrik Nyman, Andrzej Wasowski, in Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings (FoSSaCS) Editor: Roberto M. Amadio of Lecture Notes in Computer Science, vol: 4962 ©Springer-Verlag, pages: 112-126, 2008EE, PDF, BibTex, Show Abstract.
    We consider decision problems for modal and mixed transition systems used as specifications: the common implementation problem (whether a set of specifications has a common implementation), the consistency problem (whether a single specification has an implementation), and the thorough refinement problem (whether all implementations of one specification are also implementations of another one). Common implementation and thorough refinement are shown to be PSPACE-hard for modal, and so also for mixed, specifications. Consistency is PSPACE-hard for mixed, while trivial for modal specifications. We also supply upper bounds suggesting strong links between these problems.
  • Infinite Runs in Weighted Timed Automata with Energy Constraints by Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, Jiri Srba, in Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008. Proceedings (FORMATS) Editor: Franck Cassez and Claude Jard of Lecture Notes in Computer Science, vol: 5215 ©Springer-Verlag, pages: 33-47, 2008EE, PDF, BibTex, Show Abstract.
    We study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the accumulated weight. More specifically, we consider automata equipped with positive and negative weights on transitions and locations, corresponding to the production and consumption of some resource (e.g. energy). We ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (e.g. remains between 0 and some given upper-bound). We also consider a game version of the above, where certain transitions may be uncontrollable.
  • A Game-Theoretic Approach to Real-Time System Testing by Alexandre David, Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, in Design, Automation and Test in Europe, DATE 2008, Munich, Germany, March 10-14, 2008 (DATE) IEEE , pages: 486-491, 2008EE, PDF, BibTex, Show Abstract.
    This paper presents a game-theoretic approach to the testing of uncontrollable real-time systems. By modelling the systems with timed I/O game automata and specifying the test purposes as Timed CTL formulas, we employ a recently developed timed game solver UPPAAL-TIGA to synthesize winning strategies, and then use these strategies to conduct black-box conformance testing of the systems. The testing process is proved to be sound and complete with respect to the given test purposes. Case study and preliminary experimental results indicate that this is a viable approach to uncontrollable timed system testing.
  • Optimal infinite scheduling for multi-priced timed automata by Patricia Bouyer, Ed Brinksma, Kim Guldstrand Larsen, Form. Methods Syst. Des. vol: 32 ©Kluwerpages: 3--23, 2008EE, PDF, BibTex, Show Abstract.
    This paper is concerned with the derivation of infinite schedules for timed automata that are in some sense optimal. To cover a wide class of optimality criteria we start out by introducing an extension of the (priced) timed automata model that includes both costs and rewards as separate modelling features. A precise definition is then given of what constitutes optimal infinite behaviours for this class of models. We subsequently show that the derivation of optimal non-terminating schedules for such double-priced timed automata is computable. This is done by a reduction of the problem to the determination of optimal mean-cycles in finite graphs with weighted edges. This reduction is obtained by introducing the so-called corner-point abstraction, a powerful abstraction technique of which we show that it preserves optimal schedules.
  • Verification, Performance Analysis and Controller Synthesis for Real-Time Systems by Uli Fahrenberg, Kim Guldstrand Larsen, Claus Thrane, in Proceedings of the NATO Advanced Study Institute on Engineering Methods and Tools for Software Safety and Security Marktoberdorf, Germany 5-17 August 2008 (ASI 08) Editor: Manfred Broy , Wassiou Sitou and Tony Hoare of NATO Science for Peace and Security Series - D: Information and Communication Security, vol: 22 IOS Press BV , 2008BibTex, Show Abstract.
    This note aims at providing a concise and precise Travellers Guide, Phrase Book or Reference Manual to the timed automata mod- eling formalism introduced by Alur and Dill [7,8]. The note gives com- prehensive definitions of timed automata, priced (or weighted) timed automata, and timed games and highlights a number of results on asso- ciated decision problems related to model checking, equivalence checking, optimal scheduling, and winning strategies
  • Quantitative Simulations of Weighted Transition Systems by Claus Thrane, Uli Fahrenberg, Kim Guldstrand Larsen, in Proceedings of 20th Nordic Workshop of Programming Theory (NWPT) Editor: Tarmo Uustalu, Jüri Vain and Juhan Ernits, pages: 97-100, 2008 (Extended version invited for publication in Special Issue of Journal of Logic and Algebraic Programming, 2009), BibTex, Show Abstract.
    We present research motivated by the Challenge on embedded systems design, posed by Henzinger and Sifakis in [5]. Henzinger and Sifakis express the need for a co- herent theory of embedded systems design, where concern for physical constraints is supported by the computational models used to model software, thus achieving a more het- erogeneous approach to systems design. Highly distilled, Henzinger and Sifakis call for a new mathematical basis for systems modeling, which facilitates modeling of be- havioural properties as well as environmental constraints. In this work we propose a notion of weighted transi- tion systems (WTS), a quantitative extension...
  • Slicing for Uppaal by Claus Thrane, Uffe Sørensen, Kim Guldstrand Larsen, in Proceedings of 20th Nordic Workshop of Programming Theory (NWPT) Editor: Tarmo Uustalu, Jüri Vain and Juhan Ernits, pages: 100-103, 2008BibTex, Show Abstract.
    We present slicing for the model-checking tool Uppaal [5]. Slicing is a technique based on static analysis used here to reduce the syntactic size of models based on an extension of Timed Automata [1]. We show how our approach will obtain reachability preserving reductions of models, possibly improving the performance of the tool. Finally, we present the results of experimental conducted to further validate our claims...
  • Cooperative Testing of Timed Systems by Alexandre David, Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, in Proceedings of the 4th Workshop on Model-based Testing (MBT), pages: 79-92, 2008EE, BibTex, Show Abstract.
    This paper deals with targeted testing of timed systems whose models may have uncontrollable behavior. The testing activity is viewed as a game between the tester and the system under test (SUT) towards a given test purpose. The SUT is modeled as Timed Game Automaton and the test purpose is specified in Timed CTL formula. We employ a timed game solver UPPAAL-TIGA to check if the test purpose is ture w.r.t. the model, and if yes, to generate a winning strategy and use it for black-box conformance testing of the SUT implementation. Specifically, we show that in case the checking yields a negative result, we can still test the SUT implementation against the test purpose as long as the SUT implementation reacts to our moves in a cooperative style. We present an operational framework of cooperative winning strategy generation, test case derivation and execution. The test method is proved to be sound and complete. Preliminary experimental results indicate that this approach is applicable to non-trivial timed systems.
  • Approches formelles des syst`emes embarques communicant by Gerd Behrmann, Beatrice Berard, Franck Cassez, Thao Dang, Alexandre David, Susanna Donatelli, Jean-Pierre Elloy, Goran Frehse, Antoine Girard, Serge Haddad, Claude Jard, Kim Guldstrand Larsen, Colas Le Guernic, Didier Lime, Morgan Magnin, Nicolas Markey, Paul Pettersson, Jacob Illum Rasmussen, Olivier H. Roux, Stavros Tripakis, Wang Yi, Hermes Lavoisier, serie Informatique et syst`emes dinformation 2008BibTex,

2007

  • Modeling software product lines using color-blind transition systems by Kim Guldstrand Larsen, Ulrik Nyman, Andrzej Wasowski, STTT vol: 9 pages: 471-487, 2007EE, BibTex,
  • Complexity in Simplicity: Flexible Agent-Based State Space Exploration by Jacob Illum Rasmussen, Gerd Behrmann, Kim Guldstrand Larsen, in Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings (TACAS) Editor: Orna Grumberg and Michael Huth of Lecture Notes in Computer Science, vol: 4424 ©Springer-Verlag, pages: 231-245, 2007EE, BibTex,
  • Model-Checking One-Clock Priced Timed Automata by Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, in Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, Proceedings (FoSSaCS) Editor: Helmut Seidl of Lecture Notes in Computer Science, vol: 4423 ©Springer-Verlag, pages: 108-122, 2007EE, PDF, BibTex,
  • Guided Controller Synthesis for Climate Controller Using Uppaal Tiga by Jan Jakob Jessen, Jacob Illum Rasmussen, Kim Guldstrand Larsen, Alexandre David, in Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings (FORMATS) Editor: Jean-Franccois Raskin and P. S. Thiagarajan of Lecture Notes in Computer Science, vol: 4763 ©Springer-Verlag, pages: 227-240, 2007EE, BibTex,
  • Automatic Abstraction Refinement for Timed Automata by Henning Dierks, Sebastian Kupferschmid, Kim Guldstrand Larsen, in Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings (FORMATS) Editor: Jean-Franccois Raskin and P. S. Thiagarajan of Lecture Notes in Computer Science, vol: 4763 ©Springer-Verlag, pages: 114-129, 2007EE, BibTex,
  • Modal I/O Automata for Interface and Product Line Theories by Kim Guldstrand Larsen, Ulrik Nyman, Andrzej Wasowski, in Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings (ESOP) Editor: Rocco De Nicola of Lecture Notes in Computer Science, vol: 4421 ©Springer-Verlag, pages: 64-79, 2007EE, BibTex,
  • On Modal Refinement and Consistency by Kim Guldstrand Larsen, Ulrik Nyman, Andrzej Wasowski, in CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings (CONCUR) Editor: Luis Caires and Vasco Thudichum Vasconcelos of Lecture Notes in Computer Science, vol: 4703 ©Springer-Verlag, pages: 105-119, 2007EE, BibTex,
  • UPPAAL-Tiga: Time for Playing Games! by Gerd Behrmann, Agn`es Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, Didier Lime, in Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings (CAV) Editor: Werner Damm and Holger Hermanns of Lecture Notes in Computer Science, vol: 4590 ©Springer-Verlag, pages: 121-125, 2007EE, BibTex,
  • Timed Control with Observation Based and Stuttering Invariant Strategies by Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Didier Lime, Jean-Franccois Raskin, in Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings (ATVA) Editor: Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura of Lecture Notes in Computer Science, vol: 4762 ©Springer-Verlag, pages: 192-206, 2007EE, BibTex,
  • Automatic Abstraction Refinement for Timed Automata by Henning Dierks, Sebastian Kupferschmid, Kim Guldstrand Larsen, in Proceedings of Formal Modeling and Analysis of Timed Systems, 5th International Conference, (FORMATS), pages: 114-129, 2007BibTex, Show Abstract.
    We present a fully automatic approach for counterexample guided abstraction refinement of real-time systems modelled in a subset of timed automata. Our approach is implemented in the Moby/RT tool environment, which is a CASE tool for embedded system specifications. Verification in Moby/RT is done by constructing abstractions of the semantics in terms of timed automata which are fed into the model checker Uppaal. Since the abstractions are over-approximations, absence of abstract counterexamples implies a valid result for the full model. Our new approach deals with the situation in which an abstract counterexample is found by Uppaal. The generated abstract counterexample is used to construct either a crete counterexample for the full model or to identify a slightly refined abstraction in which the found spurious counterexample cannot occur anymore. Hence, the approach allows for a fully automatic abstraction refinement loop starting from the coarsest abstraction towards an abstraction for which a valid verification result is found. Nontrivial case studies demonstrate that this approach computes small abstractions fast without any user interaction. -- This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center "Automatic Verification and Analysis of Complex Systems" (SFB/TR 14 AVACS). See http://www.avacs.org/ for more information.
  • Reactive Systems: Modelling, Specification and Verification by Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen, Jiri Srba, Cambridge University Press 2007BibTex,

2006

2005

2004

  • Lower and Upper Bounds in Zone Based Abstractions of Timed Automata by Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, Radek Pelanek, in Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings (TACAS) Editor: Kurt Jensen and Andreas Podelski of Lecture Notes in Computer Science, vol: 2988 ©Springer-Verlag, pages: 312-326, 2004EE, BibTex,
  • Resource-Optimal Scheduling Using Priced Timed Automata by Jacob Illum Rasmussen, Kim Guldstrand Larsen, K. Subramani, in Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings (TACAS) Editor: Kurt Jensen and Andreas Podelski of Lecture Notes in Computer Science, vol: 2988 ©Springer-Verlag, pages: 220-235, 2004EE, BibTex,
  • A Tutorial on Uppaal by Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, in Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004, Revised Lectures (SFM) Editor: Marco Bernardo and Flavio Corradini of Lecture Notes in Computer Science, vol: 3185 ©Springer-Verlag, pages: 200-236, 2004EE, BibTex,
  • Online Testing of Real-Time Systems Using UPPAAL: Status and Future Work by Kim Guldstrand Larsen, Marius Mikucionis, Brian Nielsen, in Perspectives of Model-Based Testing, 5.-10. September 2004 (Perspectives of Model-Based Testing) Editor: Ed Brinksma and Wolfgang Grieskamp and Jan Tretmans of Dagstuhl Seminar Proceedings, vol: 04371 IBFI, Schloss Dagstuhl, Germany , 2004EE, BibTex,
  • Staying Alive as Cheaply as Possible by Patricia Bouyer, Ed Brinksma, Kim Guldstrand Larsen, in Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004, Proceedings (HSCC) Editor: Rajeev Alur and George J. Pappas of Lecture Notes in Computer Science, vol: 2993 ©Springer-Verlag, pages: 203-218, 2004EE, BibTex,
  • Optimal Strategies in Priced Timed Game Automata by Patricia Bouyer, Franck Cassez, Emmanuel Fleury, Kim Guldstrand Larsen, in FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings (FSTTCS) Editor: Kamal Lodaya and Meena Mahajan of Lecture Notes in Computer Science, vol: 3328 ©Springer-Verlag, pages: 148-160, 2004EE, BibTex,
  • Priced Timed Automata: Algorithms and Applications by Gerd Behrmann, Kim Guldstrand Larsen, Jacob Illum Rasmussen, in Formal Methods for Components and Objects, Third International Symposium, FMCO 2004, Leiden, The Netherlands, November 2 - 5, 2004, Revised Lectures (FMCO) Editor: Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem P. de Roever of Lecture Notes in Computer Science, vol: 3657 ©Springer-Verlag, pages: 162-182, 2004EE, BibTex,
  • Online Testing of Real-time Systems Using Uppaal by Kim Guldstrand Larsen, Marius Mikucionis, Brian Nielsen, in Formal Approaches to Software Testing, 4th International Workshop, FATES 2004, Linz, Austria, September 21, 2004, Revised Selected Papers (FATES) Editor: Jens Grabowski and Brian Nielsen of Lecture Notes in Computer Science, vol: 3395 ©Springer-Verlag, pages: 79-94, 2004EE, BibTex,
  • T-UPPAAL: Online Model-based Testing of Real-Time Systems by Marius Mikucionis, Kim Guldstrand Larsen, Brian Nielsen, in 19th IEEE International Conference on Automated Software Engineering (ASE 2004), 20-25 September 2004, Linz, Austria (ASE) IEEE Computer Society , pages: 396-397, 2004EE, BibTex,
  • T-UPPAAL: online model-based testing of real-time systems by Mikucionis, M., Larsen, Kim Guldstrand, Nielsen, B., in Automated Software Engineering, 2004. Proceedings. 19th International Conference on, pages: 396-397, 2004EE, BibTex, Show Abstract.
    The goal of testing is to gain confidence in a physical computer based system by means of executing it. More than one third of typical project resources are spent on testing embedded and real-time systems, but still it remains ad-hoc, based on heuristics, and error-prone. Therefore systematic, theoretically well-founded and effective automated real-time testing techniques are of great practical value. Testing conceptually consists of three activities: test case generation, test case execution and verdict assignment. We present T-UPPAAL-a new tool for model based testing of embedded real-time systems that automatically generates and executes tests önline" from a state machine model of the implementation under test (IUT) and its assumed environment which combined specify the required and allowed observable (realtime) behavior of the IUT. T-UPPAAL implements a sound and complete randomized testing algorithm, and uses a formally defined notion of correctness (relativized timed input/output conformance) to assign verdicts. Using online testing, events are generated and simultaneously executed.

2003

2002

2001

  • Guided Synthesis of Control Programs Using UPPAAL by Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Nord. J. Comput. vol: 8 pages: 43-64, 2001BibTex,
  • Verification of Large State/Event Systems Using Compositionality and Dependency Analysis by Jørn Lind-Nielsen, Henrik Reif Andersen, Henrik Hulgaard, Gerd Behrmann, Kaare J. Kristoffersen, Kim Guldstrand Larsen, Formal Methods in System Design vol: 18 pages: 5-23, 2001BibTex,
  • Reachability Analysis of Probabilistic Systems by Successive Refinements by Pedro R. DArgenio, Bertrand Jeannet, Henrik Ejersbo Jensen, Kim Guldstrand Larsen, in Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001, Aachen, Germany, September 12-14, 2001, Proceedings (PAPM-PROBMIV) Editor: Luca de Alfaro and Stephen Gilmore of Lecture Notes in Computer Science, vol: 2165 ©Springer-Verlag, pages: 39-56, 2001EE, BibTex,
  • Minimum-Cost Reachability for Priced Timed Automata by Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Judi Romijn, Frits W. Vaandrager, in Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001, Proceedings (HSCC) Editor: Maria Domenica Di Benedetto and Alberto L. Sangiovanni-Vincentelli of Lecture Notes in Computer Science, vol: 2034 ©Springer-Verlag, pages: 147-161, 2001EE, BibTex,
  • As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata by Kim Guldstrand Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, Judi Romijn, in Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings (CAV) Editor: Gerard Berry and Hubert Comon and Alain Finkel of Lecture Notes in Computer Science, vol: 2102 ©Springer-Verlag, pages: 493-505, 2001EE, BibTex,
  • Reachability Analysis of Probabilistic Systems by Successive Refinements by Pedro R. DArgenio, Bertrand Jeannet, Henrik E. Jensen, Kim Guldstrand Larsen, in Process Algebra and Probabilistic Methods. Performance Modelling and Verification, pages: 39-56, 2001EE, BibTex,
  • UPPAAL - present and future by Behrmann, G., Kim Guldstrand Larsen, Moller, O., David, A., Pettersson, P., Wang Yi, in Decision and Control, 2001. Proceedings of the 40th IEEE Conference on, pages: 2881-2886 vol.3, 2001EE, BibTex, Show Abstract.
    UPPAAL is a tool for modelling, simulation and verification of real-time systems, developed jointly by BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The tool is appropriate for systems that can be modelled as a collection of non-deterministic processes with finite control structure and real-valued clocks, communicating through channels or shared variables. Typical application areas include real-time controllers and communication protocols in particular, those where timing aspects are critical. In this paper, we review the status of the currently distributed version of the tool as well as facilities to be found in upcoming releases
  • Probabilistic Extensions of Process Algebras by Bengt Jonsson, Kim Guldstrand Larsen, Wang Yi, in Handbook of Process Algebra, pages: 685--710, 2001EE, BibTex, Show Abstract.
    Classic process, algebras such as CCS, CSP and ACP, are well-established techniques for modelling and reasoning about functional aspects of concurrent processes. The motivation for studying probabilistic extensions of process algebras is to develop techniques dealing with non-functional aspects of process behavior, such as performance and reliability. We may want to investigate, e.g., the average response time of a system, or the ? This chapter is dedicated to the fond memory of Linda Christoff. probability that a certain failure occurs. An analysis of these and similar properties requires that some form of information about the stochastic distribution over the occurrence of relevant events is put into the model. For instance, performance evaluation is often based on modeling a system as a continuous-time Markov process, in which distributions over delays between actions and over the choice between different actions are specified. Similar

2000

1999

1998

  • Model Checking via Reachability Testing for Timed Automata by Luca Aceto, Augusto Burgue no, Kim Guldstrand Larsen, in Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS 98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings (TACAS) Editor: Bernhard Steffen of Lecture Notes in Computer Science, vol: 1384 ©Springer-Verlag, pages: 263-280, 1998EE, BibTex,
  • Verification of Large State/Event Systems Using Compositionality and Dependency Analysis by Jørn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kaare J. Kristoffersen, Kim Guldstrand Larsen, in Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS 98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings (TACAS) Editor: Bernhard Steffen of Lecture Notes in Computer Science, vol: 1384 ©Springer-Verlag, pages: 201-216, 1998EE, BibTex,
  • The Power of Reachability Testing for Timed Automata by Luca Aceto, Patricia Bouyer, Augusto Burgue no, Kim Guldstrand Larsen, in Foundations of Software Technology and Theoretical Computer Science, 18th Conference, Chennai, India, December 17-19, 1998, Proceedings (FSTTCS) Editor: Vikraman Arvind and Ramaswamy Ramanujam of Lecture Notes in Computer Science, vol: 1530 ©Springer-Verlag, pages: 245-256, 1998BibTex,
  • CMC: A Tool for Compositional Model-Checking of Real-Time Systems by Franccois Laroussinie, Kim Guldstrand Larsen, in Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE XI / PSTV XVIII98, IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XI) and Protocol Specification, Testing and Verification (PSTV XVIII), 3-6 November, 1998, Paris, France (FORTE) Editor: Stanislaw Budkowski and Ana R. Cavalli and Elie Najm of IFIP Conference Proceedings, vol: 135 Kluwer , pages: 439-456, 1998BibTex,
  • The Limit of Testing for Timed Automata by L. Aceto, P. Bouyer, A. Burgueno, Kim Guldstrand Larsen, in Proceedings of Foundations of Software Technology and Theoretical Computer Science, India, 1998., 1998BibTex,
  • New Generation of UPPAAL by Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, Yi Wang, Carsten Weise, in proceedings of the International Workshop on Software Tools for Technology Transfer, 1998BibTex, Show Abstract.
    Uppaal is a tool-set for the design and analysis of real-time systems. In [6] a relatively complete description of Uppaal before 1997 has been given. This paper is focused on the most recent developments and also to complement the paper of [6]. 1 UPPAALs Past: the History The first prototype of Uppaal, named Tab at the time, was developed at Uppsala University in 1993 by Wang Yi et al. Its theoretical foundation was presented in FORTE94 [11] and the initial design was to check safety properties that can be formalized as simple reachability properties for networks of timed automata. The restriction to this simple class of properties was in sharp contrast to other real-time verification tools at that time, which where developed to check timed bisimularities or formulae of timed modal ¯-calculi. However, the ambition of catering for more complicated formulae lead to extremely severe restrictions in the size of systems that could be verified by those tools. The essential ideas behind T...

1997

  • Continuous Modeling of Real-Time and Hybrid Systems: From Concepts to Tools by Kim Guldstrand Larsen, Bernhard Steffen, Carsten Weise, STTT vol: 1 pages: 64-85, 1997EE, BibTex,
  • UPPAAL in a Nutshell by Kim Guldstrand Larsen, Paul Pettersson, Wang Yi, STTT vol: 1 pages: 134-152, 1997EE, BibTex,
  • Time-abstracted Bisimulation: Implicit Specifications and Decidability by Kim Guldstrand Larsen, Wang Yi, Inf. Comput. vol: 134 pages: 75-101, 1997BibTex,
  • A Compositional Proof of a Real-Time Mutual Exclusion Protocol by Kaare J. Kristoffersen, Franccois Laroussinie, Kim Guldstrand Larsen, Paul Pettersson, Wang Yi, in TAPSOFT97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, April 14-18, 1997, Proceedings (TAPSOFT) Editor: Michel Bidoit and Max Dauchet of Lecture Notes in Computer Science, vol: 1214 ©Springer-Verlag, pages: 565-579, 1997BibTex,
  • Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAA by Klaus Havelund, Arne Skou, Kim Guldstrand Larsen, K. Lund, in Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS 97), December 3-5, 1997, San Francisco, CA, USA (IEEE Real-Time Systems Symposium) IEEE Computer Society , pages: 2-13, 1997EE, BibTex,
  • Efficient verification of real-time systems: compact data structure and state-space reduction by Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi, in Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS 97), December 3-5, 1997, San Francisco, CA, USA (IEEE Real-Time Systems Symposium) IEEE Computer Society , pages: 14-24, 1997EE, BibTex,
  • UPPAAL: Status & Developments by Kim Guldstrand Larsen, Paul Pettersson, Wang Yi, in Computer Aided Verification, 9th International Conference, CAV 97, Haifa, Israel, June 22-25, 1997, Proceedings (CAV) Editor: Orna Grumberg of Lecture Notes in Computer Science, vol: 1254 ©Springer-Verlag, pages: 456-459, 1997BibTex,
  • Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL by Klaus Havelund, Arne Skou, Kim Guldstrand Larsen, Kristian Lund, in Proceedings of the 18th IEEE Real-Time Systems Symposium (December 03 - 05, 1997), pages: 2, 1997EE, BibTex, Show Abstract.
    A formal and automatic verification of a real-life protocol is presented. The protocol, about 2800 lines of assembler code, has been used in products from the audio/video company Bang & Olufsen throughout more than a decade, and its purpose is to control the transmission of messages between audio/video components over a single bus. Such communications may collide, and one essential purpose of the protocol is to detect such collisions. The functioning is highly dependent on real-time considerations. Though the protocol was known to be faulty in that messages were lost occasionally, the protocol was too complicated in order for Bang & Olufsen to locate the bug using normal testing. However using the real-time verification tool UPPAAL, an error trace was automatically generated, which caused the detection of "the error" in the implementation. The error was corrected and the correction was automatically proven correct, again using UPPAAL. A future, and more automated, version of the protocol, where this error is fatal, will incorporate the correction. Hence, this work is an elegant demonstration of how model checking has had an impact on practical software development. The effort of modeling this protocol has in addition generated a number of suggestions for enriching the UPPAAL language. Hence, its also an excellent example of the reverse impact.
  • Efficient verification of real-time systems: compact data structure and state-space reduction by Kim Guldstrand Larsen, F. Larsson, P. Pettersson, W. Yi, Real-Time Systems Symposium, IEEE International vol: 0 IEEE Computer Society pages: 14, 1997EE, BibTex, Show Abstract.
    During the past few years, a number of verification tools have been developed for real-time systems in the framework of timed automata (e.g. KRONOS and UPPAAL). One of the major problems in applying these tools to industrial-size systems is the huge memory-usage for the exploration of the state-space of a network (or product) of timed automata, as the model-checkers must keep information on not only the control structure of the automata but also the clock values specified by clock constraints. In this paper, we present a compact data structure for representing clock constraints. The data structure is based on an O(n/sup 3/) algorithm which, given a constraint system over real-valued variables consisting of bounds on differences, constructs an equivalent system with a minimal number of constraints. In addition, we have developed an on-the-fly, reduction technique to minimize the space-usage. Based on static analysis of the control structure of a network of timed automata, we are able to compute a set of symbolic states that cover all the dynamic loops of the network in an on-the-fly searching algorithm, and thus ensure termination in reachability analysis. The two techniques and their combination have been implemented in the tool UPPAAL. Our experimental results demonstrate that the techniques result in truly significant space-reductions: for six examples from the literature, the space saving is between 75% and 94%, and in (nearly) all examples time-performance is improved. Also noteworthy is the observation that the two techniques are completely orthogonal.
  • Context Dependent Minimization of State/Event Systems by Gerd Behrmann, KÃ¥re Kristoffersen, Kim Larsen, in Proceedings of Nordic Workshop of Programming Correctness, 1997BibTex, Show Abstract.
    This paper presents a technique for efficiently checking reachability properties of concurrent state/event systems. The technique improves the traditional algorithm for forwards exploration of the global state space by incremental construction of subsystems which are kept small using a context dependent minimization. A tool has been implemented with the specific purpose of verifying state/event systems. Experimental results reports on a feasible automatic verification of correctness of Milners Scheduler -- an often used benchmark -- with 100 cells. This result dramatically improves the previous best results for this benchmark. Also our tehcnique has been shown to perform well on industrial designs of sizes up to 400 concurrent state machines. Keywords: State/event systems; Reachability analysis; Compositionality; Subsystems; Context Dependent Minimization. 1 Introduction Model checking of finite--state concurrent systems suffers from the potential combinatorial explosion o...
  • Time Abstracted Bisimulation: Implicit Specifications and Decidability by Kim Guldstrand Larsen, Yi Wang, in Information and Computation, 1997BibTex,

1996

  • UPPAAL in 1995 by Johan Bengtsson, Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi, in Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS 96, Passau, Germany, March 27-29, 1996, Proceedings (TACAS) Editor: Tiziana Margaria and Bernhard Steffen of Lecture Notes in Computer Science, vol: 1055 ©Springer-Verlag, pages: 431-434, 1996BibTex,
  • Verification of an Audio Protocol with Bus Collision Using UPPAAL by Johan Bengtsson, W. O. David Griffioen, Kaare J. Kristoffersen, Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi, in Computer Aided Verification, 8th International Conference, CAV 96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings (CAV) Editor: Rajeev Alur and Thomas A. Henzinger of Lecture Notes in Computer Science, vol: 1102 ©Springer-Verlag, pages: 244-256, 1996BibTex,
  • Modelling and Analysis of a Collision Avoidance Protocol using SPIN and UPPAAL by Henrik Ejersbo Jensen, Jensen Kim, Kim Guldstrand Larsen, Arne Skou, in Proceedings of the 2nd International Workshop on the SPIN Verification System, 1996BibTex, Show Abstract.
    This paper compares the tools SPIN and UPPAAL by modelling and verifying a Collision Avoidance Protocol for an Ethernet--like medium. We find that SPIN is well suited for modelling the untimed aspects of the protocol processes and for expressing the relevant (untimed) properties. However, the modelling of the media becomes ackward due to the lack of broadcast communication in the PROMELA language. On the other hand we find it easy to model the timed aspects using the UPPAAL tool. Especially, the notion of committed locations supports the modelling of broadcast communication. However, the property language of UPPAAL lacks some expessivity for verification of bounded liveness properties, and we indicate how timed testing automata may be constructed for such properties, inspired by the (untimed) checking automata of SPIN. 1 Motivation During the last few years, the SPIN tool [Hol91] has attracted much interest from university people teaching formal methods and from industrial developers....

1995

  • Synthesizing Distinguishing Formulae for Real Time Systems by Jens Chr. Godskesen, Kim Guldstrand Larsen, Nord. J. Comput. vol: 2 pages: 338-357, 1995BibTex,
  • Generality in Design and Compositional Verification Using TAV by Anders Børjesson, Kim Guldstrand Larsen, Arne Skou, Formal Methods in System Design vol: 6 pages: 239-258, 1995BibTex,
  • A Constraint Oriented Proof Methodology Based on Modal Transition Systems by Kim Guldstrand Larsen, Bernhard Steffen, Carsten Weise, in Tools and Algorithms for Construction and Analysis of Systems, First International Workshop, TACAS 95, Aarhus, Denmark, May 19-20, 1995, Proceedings (TACAS) Editor: Ed Brinksma and Rance Cleaveland and Kim Guldstrand Larsen and Tiziana Margaria and Bernhard Steffen of Lecture Notes in Computer Science, vol: 1019 ©Springer-Verlag, pages: 17-40, 1995BibTex,
  • From Timed Automata to Logic - and Back by Franccois Laroussinie, Kim Guldstrand Larsen, Carsten Weise, in Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS95, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings (MFCS) Editor: Jiri Wiedermann and Petr Hajek of Lecture Notes in Computer Science, vol: 969 ©Springer-Verlag, pages: 529-539, 1995BibTex,
  • Synthesizing Distinguishing Formulae for Real Time Systems (Extended Abstract) by Jens Chr. Godskesen, Kim Guldstrand Larsen, in Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS95, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings (MFCS) Editor: Jiri Wiedermann and Petr Hajek of Lecture Notes in Computer Science, vol: 969 ©Springer-Verlag, pages: 519-528, 1995BibTex,
  • Compositional and Symbolic Model-Checking of Real-Time Systems by Kim Guldstrand Larsen, Paul Pettersson, Wang Yi, in IEEE Real-Time Systems Symposium, pages: 76-89, 1995BibTex,
  • Automatic Synthesis of Real Time Systems by Jørgen H. Andersen, Kaare J. Kristoffersen, Kim Guldstrand Larsen, Jesper Niedermann, in Automata, Languages and Programming, 22nd International Colloquium, ICALP95, Szeged, Hungary, July 10-14, 1995, Proceedings (ICALP) Editor: Zoltan Fülöp and Ferenc Gecseg of Lecture Notes in Computer Science, vol: 944 ©Springer-Verlag, pages: 535-546, 1995BibTex,
  • Fischers Protocol Revisited: A Simple Proof Using Modal Constraints by Kim Guldstrand Larsen, Bernhard Steffen, Carsten Weise, in Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA (Hybrid Systems) Editor: Rajeev Alur and Thomas A. Henzinger and Eduardo D. Sontag of Lecture Notes in Computer Science, vol: 1066 ©Springer-Verlag, pages: 604-615, 1995BibTex,
  • Diagnostic Model-Checking for Real-Time Systems by Kim Guldstrand Larsen, Paul Pettersson, Wang Yi, in Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA (Hybrid Systems) Editor: Rajeev Alur and Thomas A. Henzinger and Eduardo D. Sontag of Lecture Notes in Computer Science, vol: 1066 ©Springer-Verlag, pages: 575-586, 1995BibTex,
  • UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems by Johan Bengtsson, Kim Guldstrand Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi, in Hybrid Systems III: Verification and Control, Proceedings of the DIMACS/SYCON Workshop, October 22-25, 1995, Ruttgers University, New Brunswick, NJ, USA (Hybrid Systems) Editor: Rajeev Alur and Thomas A. Henzinger and Eduardo D. Sontag of Lecture Notes in Computer Science, vol: 1066 ©Springer-Verlag, pages: 232-243, 1995BibTex,
  • Model-Checking for Real-Time Systems by Kim Guldstrand Larsen, Paul Pettersson, Wang Yi, in Fundamentals of Computation Theory, 10th International Symposium, FCT 95, Dresden, Germany, August 22-25, 1995, Proceedings (FCT) Editor: Horst Reichel of Lecture Notes in Computer Science, vol: 965 ©Springer-Verlag, pages: 62-88, 1995BibTex,
  • Compositional Model Checking of Real Time Systems by Franccois Laroussinie, Kim Guldstrand Larsen, in CONCUR 95: Concurrency Theory, 6th International Conference, Philadelphia, PA, USA, August 21-24, 1995, Proceedings (CONCUR) Editor: Insup Lee and Scott A. Smolka of Lecture Notes in Computer Science, vol: 962 ©Springer-Verlag, pages: 27-41, 1995BibTex,
  • A refinement logic for the Fork Calculus by Havelund, Klaus, Larsen, Kim Guldstrand, in PSTV 94: Proceedings of the fourteenth of a series of annual meetings on Protocol specification, testing and verification XIV, pages: 5--20, 1995BibTex,

1994

  • The Fork Calculus by Klaus Havelund, Kim Guldstrand Larsen, Nord. J. Comput. vol: 1 pages: 346-363, 1994BibTex,
  • A refinement logic for the fork calculus by Klaus Havelund, Kim Guldstrand Larsen, in Protocol Specification, Testing and Verification XIV, Proceedings of the Fourteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Vancouver, BC, Canada, 1994 (PSTV) Editor: Son T. Vuong and Samuel T. Chanson of IFIP Conference Proceedings, vol: 1 Chapman & Hall , pages: 5-20, 1994BibTex,
  • Automatic verification of real-tim systems using epsilon by Jens Chr. Godskesen, Kim Guldstrand Larsen, Arne Skou, in Protocol Specification, Testing and Verification XIV, Proceedings of the Fourteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Vancouver, BC, Canada, 1994 (PSTV) Editor: Son T. Vuong and Samuel T. Chanson of IFIP Conference Proceedings, vol: 1 Chapman & Hall , pages: 323-330, 1994BibTex,
  • The Methodology of Modal Constraints by Kim Guldstrand Larsen, Bernhard Steffen, Carsten Weise, in Formal Systems Specification, The RPC-Memory Specification Case Study (the book grow out of a Dagstuhl Seminar, September 1994) (Formal Systems Specification) Editor: Manfred Broy and Stephan Merz and Katharina Spies of Lecture Notes in Computer Science, vol: 1169 ©Springer-Verlag, pages: 405-435, 1994BibTex,

1993

  • The Expressive Power of Implicit Specifications by Kim Guldstrand Larsen, Theor. Comput. Sci. vol: 114 pages: 119-147, 1993BibTex,
  • Time Abstracted Bisimiulation: Implicit Specifications and Decidability by Kim Guldstrand Larsen, Wang Yi, in Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings (MFPS) Editor: Stephen D. Brookes and Michael G. Main and Austin Melton and Michael W. Mislove and David A. Schmidt of Lecture Notes in Computer Science, vol: 802 ©Springer-Verlag, pages: 160-176, 1993BibTex,
  • The Fork Calculus by Klaus Havelund, Kim Guldstrand Larsen, in Automata, Languages and Programming, 20nd International Colloquium, ICALP93, Lund, Sweden, July 5-9, 1993, Proceedings (ICALP) Editor: Andrzej Lingas and Rolf G. Karlsson and Svante Carlsson of Lecture Notes in Computer Science, vol: 700 ©Springer-Verlag, pages: 544-557, 1993BibTex,
  • Model Construction for Implicit Specifications in Model Logic by Ole Høgh Jensen, Jarl Tuxen Lang, Christian Jeppesen, Kim Guldstrand Larsen, in CONCUR 93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings (CONCUR) Editor: Eike Best of Lecture Notes in Computer Science, vol: 715 ©Springer-Verlag, pages: 247-261, 1993BibTex,
  • Timed Modal Specification - Theory and Tools by Karlis Cerans, Jens Chr. Godskesen, Kim Guldstrand Larsen, in Computer Aided Verification, 5th International Conference, CAV 93, Elounda, Greece, June 28 - July 1, 1993, Proceedings (CAV) Editor: Costas Courcoubetis of Lecture Notes in Computer Science, vol: 697 ©Springer-Verlag, pages: 253-267, 1993BibTex,

1992

  • Graphical Versus Logical Specifications by Gerard Boudol, Kim Guldstrand Larsen, Theor. Comput. Sci. vol: 106 pages: 3-20, 1992BibTex,
  • A Compositional Protocol Verification Using Relativized Bisimulation by Kim Guldstrand Larsen, Robin Milner, Inf. Comput. vol: 99 pages: 80-108, 1992BibTex,
  • Testing Probabilistic and Nondeterministic Processes by Wang Yi, Kim Guldstrand Larsen, in Protocol Specification, Testing and Verification XII, Proceedings of the IFIP TC6/WG6.1 Twelth International Symposium on Protocol Specification, Testing and Verification, Lake Buena Vista, Florida, USA, 22-25 June 1992 (PSTV) Editor: Richard J. Linn Jr. and M. "Umit Uyar of IFIP Transactions, vol: C-8 North-Holland , pages: 47-61, 1992BibTex,
  • Real-Time Calculi and Expansion Theorems by Jens Chr. Godskesen, Kim Guldstrand Larsen, in NAPAW 92, Proceedings of the First North American Process Algebra Workshop, Stony Brook, New York, USA, 28 Agust 1992 (NAPAW) Editor: S. Purushothaman and Amy E. Zwarico of Workshops in Computing, ©Springer-Verlag, pages: 3-12, 1992BibTex,
  • Real-Time Calculi and Expansion Theorems by Jens Chr. Godskesen, Kim Guldstrand Larsen, in Foundations of Software Technology and Theoretical Computer Science, 12th Conference, New Delhi, India, December 18-20, 1992, Proceedings (FSTTCS) Editor: R. K. Shyamasundar of Lecture Notes in Computer Science, vol: 652 ©Springer-Verlag, pages: 302-315, 1992BibTex,
  • Generality in design and compositional verification using TAV by Anders Børjesson, Kim Guldstrand Larsen, Arne Skou, in Formal Description Techniques, V, Proceedings of the IFIP TC6/WG6.1 Fifth International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, FORTE 92, Perros-Guirec, France, 13-16 October 1992 (FORTE) Editor: Michel Diaz and Roland Groz of IFIP Transactions, vol: C-10 North-Holland , pages: 449-464, 1992BibTex,
  • Compositional Verification of Probabilistic Processes by Kim Guldstrand Larsen, Arne Skou, in CONCUR 92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings (CONCUR) Editor: Rance Cleaveland of Lecture Notes in Computer Science, vol: 630 ©Springer-Verlag, pages: 456-471, 1992BibTex,
  • Efficient Local Correctness Checking by Kim Guldstrand Larsen, in Computer Aided Verification, Fourth International Workshop, CAV 92, Montreal, Canada, June 29 - July 1, 1992, Proceedings (CAV) Editor: Gregor von Bochmann and David K. Probst of Lecture Notes in Computer Science, vol: 663 ©Springer-Verlag, pages: 30-43, 1992BibTex,

1991

  • Partial Specifications and Compositional Verification by Kim Guldstrand Larsen, Bent Thomsen, Theor. Comput. Sci. vol: 88 pages: 15-32, 1991BibTex,
  • Compositionality through an Operational Semantics of Contexts by Kim Guldstrand Larsen, Liu Xinxin, J. Log. Comput. vol: 1 pages: 761-795, 1991BibTex,
  • Bisimulation through Probabilistic Testing by Kim Guldstrand Larsen, Arne Skou, Inf. Comput. vol: 94 pages: 1-28, 1991BibTex,
  • Using Information Systems to Solve Recursive Domain Equations by Kim Guldstrand Larsen, Glynn Winskel, Inf. Comput. vol: 91 pages: 232-258, 1991BibTex,
  • On the Complexity of Equation Solving in Process Algebra by Bengt Jonsson, Kim Guldstrand Larsen, in TAPSOFT91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991, Volume 1: Colloquium on Trees in Algebra and Programming (CAAP91) (TAPSOFT, Vol.1) Editor: Samson Abramsky and T. S. E. Maibaum of Lecture Notes in Computer Science, vol: 493 ©Springer-Verlag, pages: 381-396, 1991BibTex,
  • Specification and Refinement of Probabilistic Processes by Bengt Jonsson, Kim Guldstrand Larsen, in Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, 15-18 July, 1991, Amsterdam, The Netherlands (LICS) IEEE Computer Society , pages: 266-277, 1991BibTex,
  • The Expressive Power of Implicit Specifications by Kim Guldstrand Larsen, in Automata, Languages and Programming, 18th International Colloquium, ICALP91, Madrid, Spain, July 8-12, 1991, Proceedings (ICALP) Editor: Javier Leach Albert and Burkhard Monien and Mario Rodriguez-Artalejo of Lecture Notes in Computer Science, vol: 510 ©Springer-Verlag, pages: 204-216, 1991BibTex,
  • Deciding Properties of Regular Real Time Processes by Uno Holmer, Kim Guldstrand Larsen, Wang Yi, in Computer Aided Verification, 3rd International Workshop, CAV 91, Aalborg, Denmark, July, 1-4, 1991, Proceedings (CAV) Editor: Kim Guldstrand Larsen and Arne Skou of Lecture Notes in Computer Science, vol: 575 ©Springer-Verlag, pages: 443-453, 1991BibTex,
  • Bisimulation Through Probabilistic Testing by Kim Guldstrand Larsen, Arne Skou, in Information and Control (IC91), 1991BibTex,

1990

  • Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion by Kim Guldstrand Larsen, Theor. Comput. Sci. vol: 72 pages: 265-288, 1990BibTex,
  • Equation Solving Using Modal Transition Systems by Kim Guldstrand Larsen, Liu Xinxin, in Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, 4-7 June 1990, Philadelphia, Pennsylvania, USA (LICS) IEEE Computer Society , pages: 108-117, 1990BibTex,
  • Compositionality Through an Operational Semantics of Contexts by Kim Guldstrand Larsen, Liu Xinxin, in Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, July 16-20, 1990, Proceedings (ICALP) Editor: Mike Paterson of Lecture Notes in Computer Science, vol: 443 ©Springer-Verlag, pages: 526-539, 1990BibTex,
  • Ideal Specification Formalism + Expressivity + Compositionality + Decidability + Testability + .. by Kim Guldstrand Larsen, in CONCUR 90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings (CONCUR) Editor: Jos C. M. Baeten and Jan Willem Klop of Lecture Notes in Computer Science, vol: 458 ©Springer-Verlag, pages: 33-56, 1990BibTex,
  • Graphical versus Logical Specifications by Gerard Boudol, Kim Guldstrand Larsen, in CAAP 90, 15th Colloquium on Trees in Algebra and Programming, Copenhagen, Denmark, May 15-18, 1990, Proceedings (CAAP) Editor: Andre Arnold of Lecture Notes in Computer Science, vol: 431 ©Springer-Verlag, pages: 57-71, 1990BibTex,

1989

  • Compositional Theories Based on an Operational Semantics of Contexts by Kim Guldstrand Larsen, in Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, The Netherlands, May 29 - June 2, 1989, Proceedings (REX Workshop) Editor: J. W. de Bakker and Willem P. de Roever and Grzegorz Rozenberg of Lecture Notes in Computer Science, vol: 430 ©Springer-Verlag, pages: 487-518, 1989BibTex,
  • Bisimulation Through Probabilistic Testing by Kim Guldstrand Larsen, Arne Skou, in POPL, pages: 344-352, 1989BibTex,
  • The Use of Static Constructs in A Modal Process Logic by Hans Hüttel, Kim Guldstrand Larsen, in Logic at Botik 89, Symposium on Logical Foundations of Computer Science, Pereslav-Zalessky, USSR, July 3-8, 1989, Proceedings (Logic at Botik) Editor: Albert R. Meyer and Michael A. Taitslin of Lecture Notes in Computer Science, vol: 363 ©Springer-Verlag, pages: 163-180, 1989BibTex,
  • Modal Specifications by Kim Guldstrand Larsen, in Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings (Automatic Verification Methods for Finite State Systems) Editor: Joseph Sifakis of Lecture Notes in Computer Science, vol: 407 ©Springer-Verlag, pages: 232-246, 1989BibTex,
  • TAV -- tools for automatic verification -- Users Manual by Jens Godskesen, Kim Guldstrand Larsen, Michael Zeeberg, 1989BibTex,

1988

  • Compositional Proofs by Partial Specification of Processes by Kim Guldstrand Larsen, Bent Thomsen, in Mathematical Foundations of Computer Science 1988, MFCS88, Carlsbad, Czechoslovakia, August 29 - September 2, 1988, Proceedings (MFCS) Editor: Michal Chytil and Ladislav Janiga and Vaclav Koubek of Lecture Notes in Computer Science, vol: 324 ©Springer-Verlag, pages: 414-423, 1988BibTex,
  • A Modal Process Logic by Kim Guldstrand Larsen, Bent Thomsen, in Proceedings, Third Annual Symposium on Logic in Computer Science, 5-8 July 1988, Edinburgh, Scotland, UK (LICS) IEEE Computer Society , pages: 203-210, 1988BibTex,
  • Proof System for Hennessy-Milner Logic with Recursion by Kim Guldstrand Larsen, in CAAP 88, 13th Colloquium on Trees in Algebra and Programming, Nancy, France, March 21-24, 1988, Proceedings (CAAP) Editor: Max Dauchet and Maurice Nivat of Lecture Notes in Computer Science, vol: 299 ©Springer-Verlag, pages: 215-230, 1988BibTex,

1987

1986

    1985

    • A Context Dependent Equivalence between Processes by Kim Guldstrand Larsen, in Automata, Languages and Programming, 12th Colloquium, Nafplion, Greece, July 15-19, 1985, Proceedings (ICALP) Editor: Wilfried Brauer of Lecture Notes in Computer Science, vol: 194 ©Springer-Verlag, pages: 373-382, 1985BibTex,
    • Recursively Defined Domains and Their Induction Principles by Finn Verner Jensen, Kim Guldstrand Larsen, in Foundations of Software Technology and Theoretical Computer Science, Fifth Conference, New Delhi, India, December 16-18, 1985, Proceedings (FSTTCS) Editor: S. N. Maheshwari of Lecture Notes in Computer Science, vol: 206 ©Springer-Verlag, pages: 225-245, 1985BibTex,

    1984

    • Using Information Systems to Solve Recursive Domain Equations Effectively by Glynn Winskel, Kim Guldstrand Larsen, in Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27-29, 1984, Proceedings (Semantics of Data Types) Editor: Gilles Kahn and David B. MacQueen and Gordon D. Plotkin of Lecture Notes in Computer Science, vol: 173 ©Springer-Verlag, pages: 109-129, 1984BibTex,

  • News

  • Contact

    Department of Computer Science
    Aalborg University

    Selma Lagerlöfs Vej 300,
    DK-9220 Aalborg East
    Office: 0.2.32
    Mail: kgl ‘at’ cs.aau.dk


    PHONE : +45 99 40 80 80 (Switchboard)
    PHONE : +45 99 40 88 93 (Direct)
    PHONE : +45 22 17 11 59 (Mobile)
    FAX : +45 98 15 98 89