Formal Methods and Software Engineering

Name: Formal Methods and Software Engineering | 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings

Michael Butler Sylvain Conchon Fatiha Zaïdi(Herausgeber*in)

Springer (Verlag)

Erschienen am 30. November 2015

XXV, 436 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-25423-4 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Preface
Organization
Invited Talks
Can Java Ever Be Safe? The hiJaC Project Abstract
Specification and Analysis of SoC Flows (Abstract)
Algorithmic Analysis for Asynchronous Programs
Contents
Domain-Specific Languages with Scala
1 Introduction
2 External DSLs
2.1 The Parser Library Approach
2.2 The Parser Tool Approach
3 Internal DSLs
3.1 Annotations
3.2 Shallow Embedding
3.3 Deep Embedding
4 Discussion
5 Conclusions
References
Formal Verification of Programs Computing the Floating-Point Average
1 Introduction
2 Basics About Floating-Point Arithmetic
3 Methodology and Desired Specification
3.1 Methodology
3.2 Desired Specification
4 Formal Proof of the Algorithms
4.1 The average1 Function
4.2 The average3 Function
4.3 The average2 Function
4.4 Putting All Parts Together: The Average Functions
5 Specifications and Formal Verification of the Programs
5.1 Absolute Value
5.2 Accurate Average
5.3 Correct Average
6 Conclusion and Perspectives
References
Formalization and Verification of Declarative Cloud Orchestration
1 Introduction
2 TOSCA: Topology and Orchestration Specification for Cloud Application
3 Model of Automation of Topologies
4 CafeOBJ Specification of Model
5 Verification of Setup Operation
5.1 Proof Score for Condition (1)
5.2 Cyclic Dependency
5.3 Proof Score for Condition (2)
5.4 Proof Scores for Condition (3), (4), (5) and (6)
6 Related Work and Conclusion
References
Consistency Verification of Specification Rules
1 Introduction
2 Background
2.1 Constraints Satisfiability
2.2 Rules Consistency
3 Relationship Between MISes and MUSes
4 An Efficient Algorithm for Enumerating MUSes
4.1 The MARCO algorithm
4.2 The MUSesHunter Algorithm
4.3 Comparing MARCO and MUSesHunter
5 Empirical Analysis
5.1 MUSesHunter vs. MARCO
5.2 MISes Finder
6 Conclusion
References
Applying Automata Learning to Embedded Control Software
1 Introduction
2 Engine Status Manager
2.1 ESRA
2.2 ESM and Connected Components
2.3 Rational Rose RealTime
2.4 The ESM State Diagram
3 Learning the ESM
3.1 Experimental Set-Up
3.2 Test Selection Strategies
3.3 Results
4 Verification
4.1 Approach
4.2 Model Transformations
4.3 Results
5 Conclusions and Future Work
References
A 3-Valued Contraction Model Checking Game: Deciding on the World of Partial Information
1 Introduction
2 Computation Tree Logic and Kripke Structures
2.1 Kripke Modal Transition System
2.2 KMTS as a Set of Kripke Structures
3 Semantics of CTL with Respect to KMTS
4 KMTS Operations
4.1 Dealing with Sets of KMTSs
4.2 Tree Partition Set
5 The Contraction Model Checking
6 Conclusions
References
Supporting Requirements Analysis Using Pattern-Based Formal Specification Construction
1 Introduction
2 Major Ideas of PBFSRA
2.1 Principle of PBFSRA
2.2 Procedure of Applying PBFSRA
3 Specification Pattern and System
3.1 Specification Pattern
3.2 Specification Pattern System
4 Representation of Pattern Knowledge
4.1 Attribute Tree
4.2 HFSM
5 Example
6 A Prototype Tool
7 Experiment
8 Related Work
9 Conclusions and Future Work
References
Dependency Analysis of Functional Specifications with Algebraic Data Structures
1 Introduction
1.1 A Motivating Example
2 The Modeling Language
2.1 Types and Statements
2.2 Exit Labels
2.3 The Control Flow Graph
3 Abstract Domain of Dependencies
4 Intraprocedural Analysis and Data-Flow Equations
5 Interprocedural Dependencies
6 Preliminary Results and Experiments
7 Related Work
8 Conclusion
References
A SysML Formal Framework to Combine Discrete and Continuous Simulation for Testing
1 Introduction
2 Background and Motivation
2.1 SysML Modelling Language
2.2 Model Animation and Test Generation Using CLPS-BZ
2.3 Modelica and SysML4Modelica
3 Combining Continuous and Discrete Modelling
3.1 SysML Subset for Simulation
3.2 SysML Subset for Animation and Test Generation
3.3 Combined Formalism for Simulation and Animation
4 Implementation and Case-Study Evaluation
5 Related Work
6 Conclusion and Future Work
References
Mastering the Visualization of Larger State Spaces with Projection Diagrams
1 Introduction and Motivation
2 Basic Projection Diagram Algorithm
2.1 Categorizing Edges and Equivalence Classes
2.2 Application of the Projection Diagram
3 Linking with Domain Specific Visualization
4 Related Work
5 Conclusion
References
Refinement-Based Verification of the FreeRTOS Scheduler in VCC
1 Introduction
2 ADT's and Refinement
2.1 Refinement in Z
2.2 Our Notion of Refinement
3 Viewing Z and C Models as ADT's
4 Directed Refinement Methodology
5 About FreeRTOS
6 Overview of FreeRTOS Verification
7 Details of Steps in the Verification of FreeRTOS
7.1 Z Models
7.2 Verifying that P1 Refines M2
7.3 Verifying that xList Refines xListMap
7.4 Bugs Found
8 Related Work
References
Model Checking C/OS-III Multi-task System with TMSVL
1 Introduction
2 TMSVL
2.1 Statements in TMSVL
2.2 Normal Form and Normal Form Graph for TMSVL
2.3 Timeout in TMSVL
3 C/OS-III Overview
3.1 Task Management
3.2 OS Kernel Services
4 Modeling and Verification of a C/OS-III Multi-task Application
4.1 A Multi-task Application
4.2 TMSVL Model of OS Kernel
4.3 TMSVL Model of a Multi-task System
4.4 Verification of Schedulability
5 Conclusion
References
A Predictability Algorithm for Distributed Discrete Event Systems
1 Introduction
2 Preliminaries
2.1 Models of DESs
2.2 Predictability of DESs
2.3 Sufficient and Necessary Condition
3 Centralized Framework
4 Distributed Framework
4.1 Distributed Model
4.2 Local Analysis
4.3 Global Checking
4.4 Algorithm
5 Experimental Results
6 Discussion
7 Conclusion
References
History-Based Specification and Verification of Scalable Concurrent and Distributed Systems
1 Introduction
2 The ABS Modeling Language
3 Observable Behavior
4 Deductive Verification
5 The Network-on-Chip Case Study
6 Formal Specification and Verification of the Case Study
6.1 Local Reasoning
6.2 System Specification
7 Future Work
8 Related Work
9 Conclusion
References
Regression Verification for Programmable Logic Controller Software
1 Introduction
2 Introductory Example
3 Formalizing Equivalence of PLC Programs
4 Environment Models to Increase Precision
5 Regression Verification Method and Toolchain
5.1 From PLC Code to Model Checker Input
5.2 Encoding Regression Verification
5.3 Coupling Invariants
6 Case Study
7 Related Work
8 Conclusion and Future Work
References
A Logical Approach for Behavioural Composition of Scenario-Based Models
1 Introduction
2 Interactions in UML
3 Semantics of Interactions
4 Exact Metamodel Restriction
5 Semantics of Composition
6 Composition with Alloy
7 Related Work
8 Conclusion
References
Formal Analysis of Power Electronic Systems
1 Introduction
2 Signal-Flow-Graph Theory and Mason's Gain Formula
3 Formalization of Signal-Flow-Graph and Mason's Gain
3.1 Formalization of System Properties
4 Application: Power Electronics Systems
4.1 1-Boost Cell Interleaved DC-DC Converter
4.2 Pulse Width Modulation Push-Pull DC-DC Converter
5 Conclusion
References
Practical Analysis Framework for Component Systems with Dynamic Reconfigurations
1 Introduction
2 Case Study
3 Component-Based Architecture
3.1 Configurations and Reconfigurations
3.2 Reconfiguration Model and Consistency Propagation
4 Interpreted Architecture Model
4.1 Interpreted Configurations and Reconfigurations
4.2 Compatible Interpretation
4.3 Property Preservation
5 Implementation and Architecture Conformance
5.1 Implementation Protocol
5.2 Architecture Conformance
5.3 Running Example
5.4 Other Examples
6 Related Work and Conclusion
6.1 Related Work
6.2 Conclusion
References
DFTCalc: Reliability Centered Maintenance via Fault Tree Analysis (Tool Paper)
1 Introduction
2 Fault Trees and Maintenance
3 DFTCalc
4 Experiments
5 Conclusions and Future Work
References
B for Modeling Secure Information Systems
1 Introduction
2 B4MSecure Overview
3 Translation of Functional Models
4 Extraction of An RBAC Filter from the Security Model
4.1 A Brief Overview
4.2 Case Studies
5 Conclusion
References
Enhanced Distributed Behavioral Cartography of Parametric Timed Automata
1 Introduction
2 Preliminaries
3 Static Domain Decomposition
4 Master-Worker Point Distribution Algorithms
4.1 Principle: Master-Worker
4.2 An Abstract Algorithm for the Master
4.3 Sequential Point Distribution
4.4 Random + Sequential Point Distribution
4.5 Shuffle Point Distribution
5 Dynamic Domain Decomposition
5.1 Master Algorithm
5.2 Worker Algorithm
5.3 An Additional Heuristic
6 Experiments
7 Final Remarks
References
A Recursive Probabilistic Temporal Logic
1 Introduction
2 Preliminaries
3 RPCTL
3.1 Expressive Power
4 Motivating Examples
4.1 A Token Ring Network
4.2 A Mutual Exclusion Problem
5 Model Checking
6 Related Work
7 Final Remarks
References
Specifying Compatible Sharing in Data Structures
1 Introduction
2 Motivating Examples
2.1 From Separation to Sharing
2.2 Shared Process Scheduler
2.3 Comparison with Fractional Permissions
3 Specification with Compatible Sharing
4 Verification with Compatible Sharing
5 Semantics and Soundness
5.1 Storage Model
5.2 Semantic Model of the Specification Formula
5.3 Soundness
6 Experiments
7 Related Work and Conclusions
References
Delta-Oriented FSM-Based Testing
1 Introduction
2 Related Work
3 Preliminaries
3.1 FSM-Based Testing
3.2 Delta-Oriented Syntactic Structure
4 Running Example
5 Delta-Oriented FSM Modeling
5.1 Core Model Semantics
5.2 Delta Application
6 Delta-Oriented Testing
6.1 Test-Case Generation for Class Addition
7 Empirical Results
8 Conclusions and Future Work
References
An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems
1 Introduction
2 Isabelle/HOL
3 Hybrid CSP
3.1 Syntax
3.2 Operational Semantics
3.3 Hybrid Hoare Logic
4 HHL Prover: Shallow Embedding
4.1 HCSP
4.2 Assertion Languages
4.3 Specification and Inference Rules
5 HHL Prover: Deep Embedding
5.1 Assertion Languages
6 A Case Study
6.1 Description of the Control Program
6.2 Verification in HHL Prover
7 Conclusion
References
Continuation Semantics for Concurrency with Multiple Channels Communication
1 Introduction
2 MCC Syntax and Continuation Structure
2.1 Continuation Structure for MCC
3 Denotational Semantics
3.1 Concurrency Laws
4 Operational Semantics (O): Relating D and O
5 Conclusion
References
SysML Blocks Adaptation
1 Introduction
2 Related Work
3 Background
3.1 Block Definition Diagram
3.2 Internal Block Diagram
3.3 Interface Automata
3.4 Adaptation contract
4 Proposed Approach
4.1 The First Phase: Compute the Adapter Interaction Protocol
4.2 The Second Phase: Construct the SysML Adapter Block
4.3 The Third Phase: Build the BDD and the IBD of the Block B
5 Case Study
5.1 The First Phase: Compute the IA_adapter
5.2 The Second Phase: Construct the SysML Adapter Block
5.3 The Third Phase: Construct the BDD and the IBD
6 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken