This volume contains the proceedings of FORTE 2003, the 23rd IFIP TC 6/ WG 6.1 International Conference on Formal Techniques for Networked and D- tributed Systems, held in Berlin, Germany, September 29–October 2, 2003. FORTE denotes a series of international working conferences on formal descr- tion techniques (FDTs) applied to computer networks and distributed systems. The conference series started in 1981 under the name PSTV. In 1988 a s- ond series under the name FORTE was set up. Both series were united to FORTE/PSTV in 1996. Two years ago the conference name was changed to its current form. The last ?ve meetings of this long conference series were held in Paris, France (1998), Beijing, China (1999), Pisa, Italy (2000), Cheju Island, Korea (2001), and Houston, USA (2002). The 23rd FORTE conference was especially dedicated to the application of formal description techniques to practice, especially in the Internet and c- munication domain. The scope of the papers presented at FORTE 2003 covered the application of formal techniques, timed automata, FDT-based design, v- i?cation and testing of communication systems and distributed systems, and the veri?cation of security protocols. In addition, work-in-progress papers were presented which have been published in a separate volume.
Author(s): Paweł Rychwalski, Jacek Wytrębowicz (auth.), Hartmut König, Monika Heiner, Adam Wolisz (eds.)
Series: Lecture Notes in Computer Science 2767
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2003
Language: English
Pages: 429
Tags: Computer Communication Networks; Software Engineering; Operating Systems; Logics and Meanings of Programs
Front Matter....Pages -
UNIX STREAMS Generation from a Formal Specification....Pages 1-14
Specifying and Realising Interactive Voice Services....Pages 15-30
Vertical Reuse in the Development of Distributed Systems with FDTs....Pages 31-47
Service-Oriented Systems Engineering: Modeling Services and Layered Architectures....Pages 48-61
Validation of the Sessionless Mode of the HTTPR Protocol....Pages 62-78
Generation of All Counter-Examples for Push-Down Systems....Pages 79-94
Modeling and Model Checking Mobile Phone Payment Systems....Pages 95-110
Behavioural Contracts for a Sound Assembly of Components....Pages 111-126
Automatic Verification of Annotated Code....Pages 127-143
Combating Infinite State Using Ergo....Pages 144-159
Numerical Coverage Estimation for the Symbolic Simulation of Real-Time Systems....Pages 160-176
Discrete Timed Automata and MONA: Description, Specification and Verification of a Multimedia Stream....Pages 177-192
Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification?....Pages 193-208
How Stop and Wait Protocols Can Fail over the Internet....Pages 209-223
Introducing Commutative and Associative Operators in Cryptographic Protocol Analysis....Pages 224-239
A Lightweight Formal Analysis of a Multicast Key Management Scheme....Pages 240-256
Formal Security Policy Verification of Distributed Component-Structured Software....Pages 257-272
Towards Testing SDL Specifications: Models and Fault Coverage for Concurrent Timers....Pages 273-288
Concerning the Ordering of Adaptive Test Sequences....Pages 289-302
Correct Passive Testing Algorithms and Complete Fault Coverage....Pages 303-318
QoS Functional Testing for Multi-media Systems....Pages 319-334
Towards Testing Stochastic Timed Systems....Pages 335-350
Formal Design of Interactive Multimedia Documents....Pages 351-366
Progressive Solutions to a Parallel Automata Equation....Pages 367-382
Type Abstraction in Formal Protocol Specifications with Container Types....Pages 383-398
Decomposing Service Definition in Predicate/Transition-Nets for Designing Distributed Systems....Pages 399-414
Towards an Efficient Performance Evaluation of Communication Systems Described by Message Sequence Charts....Pages 415-429
Back Matter....Pages -
