FME 2003: Formal Methods International Symposium of Formal Methods Europe. Pisa Italy, September 8-14, 2003, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Araki, Keijiro (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Gnesi, Stefania (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Mandrioli, Dion (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2003.
• Έκδοση: 1st ed. 2003.
• Σειρά: Lecture Notes in Computer Science, 2805
• Θέματα: Software engineering.; Computer logic.; Computer programming.; Programming languages (Electronic computers).; Mathematical logic.; Software Engineering/Programming and Operating Systems.; Logics and Meanings of Programs.; Programming Techniques.; Software Engineering.; Programming Languages, Compilers, Interpreters.; Mathematical Logic and Formal Languages.

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...

Πίνακας περιεχομένων:

• 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 Reactive Object-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.