Muutke küpsiste eelistusi

E-raamat: FM 2005: Formal Methods: International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings

Edited by , Edited by
  • Formaat: PDF+DRM
  • Sari: Lecture Notes in Computer Science 3582
  • Ilmumisaeg: 25-Aug-2005
  • Kirjastus: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • Keel: eng
  • ISBN-13: 9783540317142
Teised raamatud teemal:
  • Formaat - PDF+DRM
  • Hind: 55,56 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.
  • Formaat: PDF+DRM
  • Sari: Lecture Notes in Computer Science 3582
  • Ilmumisaeg: 25-Aug-2005
  • Kirjastus: Springer-Verlag Berlin and Heidelberg GmbH & Co. K
  • Keel: eng
  • ISBN-13: 9783540317142
Teised raamatud teemal:

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

This volume contains the proceedings of Formal Methods 2005, the 13th InternationalSymposiumonFormalMethodsheldinNewcastleuponTyne,UK, during July 1822, 2005. Formal Methods Europe (FME, www.fmeurope.org) is an independent association which aims to stimulate the use of, and research on, formal methods for system development. FME conferences began with a VDM Europe symposium in 1987. Since then, the meetings have grown and have been held about once every 18 months. Throughout the years the symposia have been notablysuccessfulinbringingtogetherresearchers,tooldevelopers,vendors,and users, both from academia and from industry. Formal Methods 2005 con rms this success. We received 130 submissions to the main conference, from all over the world. Each submission was carefully refereed by at least three reviewers. Then, after an intensive, in-depth discussion, the Program Committee selected 31 papers for presentation at the conference. They form the bulk of this volume. We would like to thank all the Program Committee members and the referees for their excellent and e cient work. Apart from the selected contributions, the Committee invited three keynote lectures from Mathai Joseph, Marie-Claude Gaudel and Chris Johnson. You will ?nd the abstracts/papers for their keynote lectures in this volume as well. AninnovationfortheFM2005programwasapaneldiscussiononthehistory of formal methods, with Jean-Raymond Abrial, Dines Bjørner, Jim Horning and Cli? Jones as panelists. Unfortunately, it was not possible to re ect this event in the current volume, but you will ?nd the material documenting it elsewhere (see the conference Web page).
Keynote Talks
Formal Aids for the Growth of Software Systems
1(1)
Mathai Joseph
Formal Methods and Testing: Hypotheses, and Correctness Approximations
2(7)
Marie-Claude Gaudel
The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions
9(17)
C. W. Johnson
Object Orientation
Modular Verification of Static Class Invariants
26(17)
K. Rustan
M. Leino
Peter Muller
Decoupling in Object Orientation
43(16)
Ioannis T. Kassios
Controlling Object Allocation Using Creation Guards
59(16)
Cees Pierik
Dave Clarke
Frank S. de Boer
Symbolic Animation of JML Specifications
75(16)
Fabrice Bouquet
Frederic Dadeau
Bruno Legeard
Mark Utting
Resource Analysis and Verification
Certified Memory Usage Analysis
91(16)
David Cachera
Thomas Jensen
David Pichardie
Gerardo Schneider
Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs
107(16)
Orieta Celiku
Annabelle McIver
Formally Defining and Verifying Master/Slave Speculative Parallelization
123(16)
Pierre Salverda
Grigore Rosu
Craig Zilles
Timing and Testing
Systematic Implementation of Real-Time Models
139(18)
Martin De Wulf
Laurent Doyen
Jean-Francois Raskin
Timing Tolerances in Safety-Critical Software
157(16)
Alan Wassyng
Mark Lawford
Xiayong Hu
Timed Testing with TorX
173(16)
Henrik Bohnenkamp
Axel Belinfante
Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems
189(16)
Vlad Rusu
Herve Marchand
Thierry Jeron
CSP, B and Circus
Adding Conflict and Confusion to CSP
205(16)
Christie Bolton
Combining CSP and B for Specification and Property Verification
221(16)
Michael Butler
Michael Leuschel
Operational Semantics for Model Checking Circus
237(16)
Jim Woodcock
Ana Cavalcanti
Leonardo Freitas
Control Law Diagrams in Circus
253(16)
Ana Cavalcanti
Phil Clayton
Colin O'Halloran
Security
Verification of a Signature Architecture with HOL-Z
269(17)
David Basin
Hironobu Kuruma
Kazuo Takaragi
Burkhart Wolff
End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform
286(16)
Mikael Buchholtz
Stephen Gilmore
Valentin Haenel
Carlo Montangero
Formal Verification of Security Properties of Smart Card Embedded Source Code
302(16)
June Andronick
Boutheina Chetali
Christine Paulin-Mohring
Networks and Processes
A Formal Model of Addressing for Interoperating Networks
318(16)
Pamela Zave
An Approach to Unfolding Asynchronous Communication Protocols
334(16)
Yu Lei
S. Purushothaman Iyer
Semantics of BPEL4WS-Like Fault and Compensation Handling
350(16)
Qiu Zongyan
Wang Shuling
Pu Geguang
Zhao Xiangpeng
Abstraction, Retrenchment and Rewriting
On Some Galois Connection Based Abstractions for the Mu-Calculus
366(16)
Dragan Bosnacki
Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern
382(17)
Richard Banach
Michael Poppleton
Czeslaw Jeske
Susan Stepney
Strategic Term Rewriting and Its Application to a VDM-SL to SQL Conversion
399(16)
T.L. Alves
P.F. Silva
J. Visser
J.N. Oliveira
Scenarios and Modeling Languages
Synthesis of Distributed Processes from Scenario-Based Specifications
415(17)
Jun Sun
Jin Song Dong
Verifying Scenario-Based Aspect Specifications
432(16)
Emilia Katz
Shmuel Katz
An MDA Approach Towards Integrating Formal and Informal Modeling Languages
448(17)
Soon-Kyeong Kim
Damian Burger
David Carrington
Model Checking
Model-Checking of Specifications Integrating Processes, Data and Time
465(16)
Jochen Hoenicke
Patrick Maier
Automatic Symmetry Detection for Model Checking Using Computational Group Theory
481(16)
A.F. Donaldson
A. Miller
On Partitioning and Symbolic Model Checking
497(15)
Subramanian Iyer
Debashis Sahoo
E. Allen Emerson
Jawahar Jain
Dynamic Component Substitutability Analysis
512(17)
Natasha Sharygina
Sagar Chaki
Edmund Clarke
Nishant Sinha
Industry Day: Abstracts of Invited Talks
Floating-Point Verification
529(4)
John Harrison
Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications
533(4)
Stefan Eisler
Christian Scheidler
Bernhard Josko
Guido Sandmann
Joachim Stroop
Model-Based Testing in Practice
537(5)
Alexander Pretschner
Testing Concurrent Object-Oriented Systems with Spec Explorer
542(6)
Colin Campbell
Wolfgang Grieskamp
Lev Nachmanson
Wolfram Schulte
Nikolai Tillmann
Margus Veanes
ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software
548(4)
Guy H. Broadfoot
The Informal Nature of Systems Engineering
552(5)
Gerrit Muller
Author Index 557