+612 9045 4394
Formal Methods for Real-Time and Probabilistic Systems : 5th International Amast Workshop, Arts'99, Bamberg, Germany, May 26-28, 1999, Proceedings - Jost-Pieter Katoen

Formal Methods for Real-Time and Probabilistic Systems

5th International Amast Workshop, Arts'99, Bamberg, Germany, May 26-28, 1999, Proceedings

By: Jost-Pieter Katoen (Editor)


Published: 12th May 1999
Ships: 15 business days
15 business days
or 4 easy payments of $33.88 with Learn more

TheaimoftheARTS'99workshopistobringtogetherresearchersandpr- titioners interested in the design of real-time and probabilistic systems. It is intendedtocoverthewholespectrumofdevelopmentandapplicationofspec- cation, veri cation, analysisandconstructiontechniquesforreal-timeandpro- bilisticsystems. BeingaworkshopundertheumbrellaoftheAMASTmovement (AlgebraicMethodologyAndSoftwareTechnology), ARTSisintendedtoprovide aforumforthepresentationofapproachesthatarebasedonaclearmathema- calbasis. Aspectsofreal-timeandprobabilisticsystemsfortheworkshopinclude (butarenotlimitedto): compositionalconstructionandveri cationtechniques, automaticandmachine-supportedveri cation, casestudies, formalmethodsfor performanceanalysis, semantics, algorithmsandtools, andhybridsystems. ARTS'99wasorganisedbytheLehrstuhlfur ] Informatik7attheUniversity ofErlangen-Nurn ] bergandtookplaceattheSt]adtlicheVolkshochschuleinB- berg(Oberfranken), GermanyfromMay26{28,1999. PreviouseditionsofARTS workshopswereorganizedbytheUniversityofIowa, USA(1993), Universityof Bordeaux, France(1995), BrighamYoungUniversity, USA(1996), andGeneral SystemsDevelopment, Mallorca, Spain(1997). Previousproceedingsappeared asLNCS1231orasbooksintheAMASTSeriesofComputing. TheProgramCommitteeselected17papersfromatotalof33submissions. Each submitted paper was sent to three Program Committee members, who wereoftenassistedbysub-referees. Duringaone-weekdiscussionviae-mail, the ProgramCommitteehasmadetheselectionofthepapersonthebasisofthe reviews. Thisvolumecontainsthe17selectedpapersplus3invitedpapers(in eitherfullorabstractform). IwouldliketothanktheProgramCommitteemembersandthesub-referees fortheire orts. Ialsoliketothanktheinvitedspeakersforgivingatalkatthe workshopandfortheircontributiontotheproceedings. SpecialthankstoUlrich Herzog, ChrisMoog, TeodorRus, DiegoLatellaandRuthAbraham(Springer- Verlag)fortheirsupport. Withouttheirhelp, thiseventwouldnothavebeen possible. March1999 Joost-PieterKatoen ProgramChair ARTS'99 Invited Speakers Bengt Jonsson (Uppsala University, Sweden) Frits W. Vaandrager(University of Nijmegen, The Netherlands) Moshe Y. Vardi (Rice University, USA) Steering Committee Manfred Broy (Technical University of Munich, Germany) Edmund Clarke (Carnegie Mellon University, USA) Ulrich Herzog (University of Erlangen-Nu ]rnberg, Germany) Zohar Manna (Stanford University, USA) Maurice Nivat (University of Paris 6, France) Amir Pnueli (Weizmann Institute of Science, Israel) Teodor Rus (Chair, University of Iowa, USA) ProgramCommittee Rajeev Alur (University of Pennsylvania, USA) Jos Baeten (Eindhoven University of Technology, The Netherlands) Christel Baier (University of Mannheim, Germany) Miquel Bertran (University of Ramon Llull, Spain) Antonio Cerone (University of South Australia, Australia) Rance Cleaveland (SUNY at Stony Brook, USA) Jim Davies (Oxford University, UK) Colin Fidge (University of Queensland, Australia) David de Frutos (University of Madrid, Spain) Hubert Garavel (INRIA Rhone-Alpes, France) Constance Heitmeyer (Naval Research Laboratory, USA) Tom Henzinger (University of Berkeley, USA) Jane Hillston (University of Edinburgh, UK) Joost-Pieter Katoen (University of Erlangen-Nu ]rnberg, Germany, Chair) Rom Langerak (University of Twente, The Netherlands) Kim G.

Fully Abstract Characterization of Probabilistic May Testingp. 1
Quantitative Program Logic and Performance in Probabilistic Distributed Algorithmsp. 19
Establishing Qualitative Properties for Probabilistic Lossy Channel Systems: An Algorithmic Approachp. 34
Root Contention in IEEE 1394p. 53
Automatic Verification of Real-Time Systems with Discrete Probability Distributionsp. 75
ProbVerus: Probabilistic Symbolic Model Checkingp. 96
Process Algebra with Probabilistic Choicep. 111
An Axiomatization of Probabilistic Testingp. 130
Verification of Hybrid Systemsp. 151
A Parallel Operator for Real-Time Processes with Predicate Transformer Semanticsp. 152
Comparing the Efficiency of Asynchronous Systemsp. 172
A Formal Model of Real-Time Program Compilationp. 192
Specifying Performance Measures for PEPAp. 211
Semi-numerical Solution of Stochastic Process Algebra Modelsp. 228
Bisimulation Algorithms for Stochastic Process Algebras and Their BDD-Based Implementationp. 244
Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approachp. 265
Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaalp. 277
Verifying Progress in Timed Systemsp. 299
Proof Assistance for Real-Time Systems Using an Interactive Theorem Proverp. 315
Modelling Timeouts without Timelocksp. 334
Author Indexp. 355
Table of Contents provided by Blackwell. All Rights Reserved.

ISBN: 9783540660101
ISBN-10: 3540660100
Series: Lecture Notes in Physics,
Audience: General
Format: Paperback
Language: English
Number Of Pages: 353
Published: 12th May 1999
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: US
Dimensions (cm): 23.39 x 15.6  x 1.96
Weight (kg): 0.52