FME 2003 : formal methods : International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003 : proceedings
ThisvolumecontainstheproceedingsofFM2003,the12thInternationalFormal Methods Europe Symposium which was held in Pisa, Italy on September 8 14, 2003. Formal Methods Europe (FME, www. fmeurope. org) is an independent - sociation which aims to stimulate the use of and research on formal methods for syst...
保存先:
| 団体著者: | |
|---|---|
| その他の著者: | , , |
| フォーマット: | Livre numérique |
| 言語: | Anglais |
| 出版事項: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| シリーズ: | Lecture notes in computer science
2805 |
| 主題: | |
| オンライン･アクセス: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| 注記: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • FME 2003, formal methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, proceedings, Keijiro Araki, Stefania Gnesi, Dino Mandrioli, 2003, Berlin, Springer, 1 vol. (XVII-942 p.), Lecture notes in computer science, 3-540-40828-2 • FME 2003: Formal Methods, Texte imprimé, 9783662170489 |
目次:
- Invited Speakers
- Looking Back to the Future
- Past, Present, and Future of SRA Implementation of CafeOBJ
- On Failures and Faults
- Trends in Software Verification
- Event Based Sequential Program Development: Application to Constructing a Pointer Program
- I-Day
- Proving the Shalls
- Adaptable Translator of B Specifications to Embedded C Programs
- Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle
- Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project
- Control Systems and Industrial Applications
- Determining the Specification of a Control System from That of Its Environment
- Managerial Issues for the Consideration and Use of Formal Methods
- Verifying Emulation of Legacy Mission Computer Systems
- Improving Safety Assessment of Complex Systems: An Industrial Case Study
- Communications System Verification
- Compositional Verification of an ATM Protocol
- Proving the Correctness of Simpson s 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method
- Synthesis and Verification of Constraints in the PGM Protocol
- Co-specification and Compilers
- Mapping Statecharts to Verilog for Hardware/Software Co-specification
- A Strategy for Compiling Classes, Inheritance, and Dynamic Binding
- Composition
- A Semantic Foundation for TCOZ in Unifying Theories of Programming
- Refinement and Verification of Synchronized Component-Based Systems
- Certifying and Synthesizing Membership Equational Proofs
- Team Automata Satisfying Compositionality
- Composing Invariants
- Java, Object Orientation and Modularity
- Java Applet Correctness: A Developer-Oriented Approach
- Improving JML: For a Safer and More Effective Language
- Using Abstractions for Heuristic State Space Exploration of ReactiveObject-Oriented Systems
- A Formal Framework for Modular Synchronous System Design
- Model Checking
- Generating Counterexamples for Multi-valued Model-Checking
- Combining Real-Time Model-Checking and Fault Tree Analysis
- Model-Checking TRIO Specifications in SPIN
- Computing Meta-transitions for Linear Transition Systems with Polynomials
- Translation-Based Compositional Reasoning for Software Systems
- Watchdog Transformations for Property-Oriented Model-Checking
- Parallel Process
- A Circus Semantics for Ravenscar Protected Objects
- Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach
- A General Approach to Deadlock Freedom Verification for Software Architectures
- Taking Alloy to the Movies
- Interacting State Machines for Mobility
- Composing Temporal-Logic Specifications with Machine Assistance
- Program Checking and Testing
- Model Checking FTA
- Program Checking with Certificates: Separating Correctness-Critical Code
- Reification of Executable Test Scripts in Formal Specification-Based Test Generation: The Java Card Transaction Mechanism Case Study
- Checking and Reasoning about Semantic Web through Alloy
- B Method
- Structuring Retrenchments in B by Decomposition
- Design of an Automatic Prover Dedicated to the Refinement of Database Applications
- ProB: A Model Checker for B
- Security
- SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis
- Correctness of Source-Level Safety Policies
- A Topological Characterization of TCP/IP Security.