FM 2005 : formal methods : International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005 : proceedings / / John Fitzgerald, Ian J. Hayes, Andrzej Tarlecki (eds.) |
Edizione | [1st ed. 2005.] |
Pubbl/distr/stampa | Berlin ; ; New York, : Springer, 2005 |
Descrizione fisica | 1 online resource (XIV, 558 p.) |
Disciplina | 004.13/1 |
Altri autori (Persone) |
FitzgeraldJohn <1965->
HayesIan TarleckiAndrzej |
Collana | Lecture notes in computer science |
Soggetto topico |
Computer software - Development
Formal methods (Computer science) System design |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Keynote Talks -- Formal Aids for the Growth of Software Systems -- Formal Methods and Testing: Hypotheses, and Correctness Approximations -- The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions -- Object Orientation -- Modular Verification of Static Class Invariants -- Decoupling in Object Orientation -- Controlling Object Allocation Using Creation Guards -- Symbolic Animation of JML Specifications -- Resource Analysis and Verification -- Certified Memory Usage Analysis -- Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs -- Formally Defining and Verifying Master/Slave Speculative Parallelization -- Timing and Testing -- Systematic Implementation of Real-Time Models -- Timing Tolerances in Safety-Critical Software -- Timed Testing with TorX -- Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems -- CSP, B and Circus -- Adding Conflict and Confusion to CSP -- Combining CSP and B for Specification and Property Verification -- Operational Semantics for Model Checking Circus -- Control Law Diagrams in Circus -- Security -- Verification of a Signature Architecture with HOL-Z -- End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform -- Formal Verification of Security Properties of Smart Card Embedded Source Code -- Networks and Processes -- A Formal Model of Addressing for Interoperating Networks -- An Approach to Unfolding Asynchronous Communication Protocols -- Semantics of BPEL4WS-Like Fault and Compensation Handling -- Abstraction, Retrenchment and Rewriting -- On Some Galois Connection Based Abstractions for the Mu-Calculus -- Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern -- Strategic Term Rewriting and Its Application to a Vdm-sl to Sql Conversion -- Scenarios and Modeling Languages -- Synthesis of Distributed Processes from Scenario-Based Specifications -- Verifying Scenario-Based Aspect Specifications -- An MDA Approach Towards Integrating Formal and Informal Modeling Languages -- Model Checking -- Model-Checking of Specifications Integrating Processes, Data and Time -- Automatic Symmetry Detection for Model Checking Using Computational Group Theory -- On Partitioning and Symbolic Model Checking -- Dynamic Component Substitutability Analysis -- Industry Day: Abstracts of Invited Talks -- Floating-Point Verification -- Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications -- Model-Based Testing in Practice -- Testing Concurrent Object-Oriented Systems with Spec Explorer -- ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software -- The Informal Nature of Systems Engineering. |
Altri titoli varianti |
Formal methods 2005
International Symposium of Formal Methods Europe FME Formal methods Europe |
Record Nr. | UNINA-9910483583503321 |
Berlin ; ; New York, : Springer, 2005 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
FM 2005: Formal Methods [[electronic resource] ] : International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings / / edited by John Fitzgerald, Ian J. Hayes |
Edizione | [1st ed. 2005.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
Descrizione fisica | 1 online resource (XIV, 558 p.) |
Disciplina | 004.13/1 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Computer logic Programming languages (Electronic computers) Computer programming Mathematical logic Management information systems Computer science Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Programming Techniques Mathematical Logic and Formal Languages Management of Computing and Information Systems |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Keynote Talks -- Formal Aids for the Growth of Software Systems -- Formal Methods and Testing: Hypotheses, and Correctness Approximations -- The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions -- Object Orientation -- Modular Verification of Static Class Invariants -- Decoupling in Object Orientation -- Controlling Object Allocation Using Creation Guards -- Symbolic Animation of JML Specifications -- Resource Analysis and Verification -- Certified Memory Usage Analysis -- Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs -- Formally Defining and Verifying Master/Slave Speculative Parallelization -- Timing and Testing -- Systematic Implementation of Real-Time Models -- Timing Tolerances in Safety-Critical Software -- Timed Testing with TorX -- Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems -- CSP, B and Circus -- Adding Conflict and Confusion to CSP -- Combining CSP and B for Specification and Property Verification -- Operational Semantics for Model Checking Circus -- Control Law Diagrams in Circus -- Security -- Verification of a Signature Architecture with HOL-Z -- End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform -- Formal Verification of Security Properties of Smart Card Embedded Source Code -- Networks and Processes -- A Formal Model of Addressing for Interoperating Networks -- An Approach to Unfolding Asynchronous Communication Protocols -- Semantics of BPEL4WS-Like Fault and Compensation Handling -- Abstraction, Retrenchment and Rewriting -- On Some Galois Connection Based Abstractions for the Mu-Calculus -- Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern -- Strategic Term Rewriting and Its Application to a Vdm-sl to Sql Conversion -- Scenarios and Modeling Languages -- Synthesis of Distributed Processes from Scenario-Based Specifications -- Verifying Scenario-Based Aspect Specifications -- An MDA Approach Towards Integrating Formal and Informal Modeling Languages -- Model Checking -- Model-Checking of Specifications Integrating Processes, Data and Time -- Automatic Symmetry Detection for Model Checking Using Computational Group Theory -- On Partitioning and Symbolic Model Checking -- Dynamic Component Substitutability Analysis -- Industry Day: Abstracts of Invited Talks -- Floating-Point Verification -- Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications -- Model-Based Testing in Practice -- Testing Concurrent Object-Oriented Systems with Spec Explorer -- ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software -- The Informal Nature of Systems Engineering. |
Record Nr. | UNISA-996465825403316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|