Formal Methods: Foundations and Applications

Name: Formal Methods: Foundations and Applications | 19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23-25, 2016, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23-25, 2016, Proceedings

Leila Ribeiro Thierry Lecomte(Herausgeber*in)

Springer (Verlag)

Erschienen am 12. November 2016

X, 253 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-49815-7 (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
Contents
Invited Talks
Formal Model-Based Constraint Solving and Document Generation
1 Animation and Constraint Solving for B
2 Model-Based Constraint Solving
3 Model-Based Document Generation
4 A Portfolio of Constraint Solving Examples in B
4.1 Graph Colouring
4.2 Graph Isomorphism
4.3 N-Queens and Bishops
4.4 Golomb Ruler
4.5 Sudoku and Latin Squares
4.6 Coins Puzzle
5 External Data Sources and Data Validation
5.1 External Data Sources
5.2 Data Validation Example
6 Discussion
References
Formal Testing from Natural Language in an Industrial Context
1 Overview
2 Tools
2.1 Test Generation with TaRGeT
2.2 Test Automation with Zygon
3 Underlying Formalisms
3.1 Process Algebraic Approach to Test Generation
3.2 Contract Based Approach to Consistent Automation
4 Ongoing Work: Integrated Framework
References
Analysis and Verification
Application of Formal Methods to Verify Business Processes
1 Introduction
2 Theoretical Framework
2.1 Timed Automata (TA)
2.2 Business Process Model and Notation (BPMN)
2.3 Clocked Computation Tree Logic (CCTL)
3 BP-Task Model
4 Mapping Rules to Specify and Verify BPMN Models Using TA
5 CRM Application Example
5.1 CRM Task Model
5.2 CRM Properties
5.3 CRM Verification
6 Conclusion and Future Work
References
An Approach for Verifying Educational Robots
1 Introduction
2 Simulating Robot Programs
2.1 Overview of the Verification Approach
3 Formalising the Robot
3.1 Communicating Sequential Processes
3.2 Robot Formal Specification
4 Verifying Robot Programs
5 Integrating the Approach with Educational Tools
6 Conclusions
References
Verigraph: A System for Specification and Analysis of Graph Grammars
1 Introduction
2 Algebraic Graph Transformation
2.1 Example
2.2 Generalization and Other Approaches
3 Architecture Overview and Data Structures
4 Implemented Analysis Techniques
4.1 Critical Pair Analysis
4.2 Critical Sequence Analysis
4.3 Calculation of Concurrent Rules
4.4 State Space Exploration and Model Checking
4.5 Inter-Level Conflict Analysis
5 Related Work
5.1 AGG
5.2 GROOVE
5.3 Preliminary Performance Evaluation
6 Conclusions
References
Modeling and Logic
Modelling `Operation-Calls' in Event-B with Shared-Event Composition
1 Introduction
2 Event-B
3 An Overview of Event-B Components
4 Procedure-Style Interface Events
4.1 Procedural Interface Events
4.2 Translation of the Call
4.3 The Combined Event Representation
5 Function-Style Interface Events for Use in Expressions
5.1 Functional Interface Events
5.2 Translation of the Call
5.3 The Combined Event Representation
6 Discussion and Related Work
6.1 A Comparison with the Modularisation Approach -- in More Detail
7 Conclusions
References
Algebraic Foundations for Specification Refinements
1 Introduction
2 Preliminaries
3 A Category of Refinements
3.1 Heterogeneous Refinements
4 Data Refinement
5 Related Work and Conclusions
References
On Interval Dynamic Logic
1 Introduction
2 An L-Fuzzy Dynamic Logic
2.1 The Lukasiewicz Action Lattice
2.2 The L-Fuzzy Dynamic Logic
3 L-Interval Algebra
3.1 On the Interval Lukasiewicz Lattice
4 The Price
5 Conclusion and Further Work
References
An Evolutionary Approach to Translate Operational Specifications into Declarative Specifications
1 Introduction
2 A Motivating Example
3 An Evolutionary Algorithm for Learning Declarative Specifications
3.1 Genes and Chromosomes to Represent Candidate Specifications
3.2 Fitness of Candidate Specifications
3.3 Overall Structure of the Genetic Algorithm for Learning Specifications
4 Validation
4.1 Assessment
5 Related Work
6 Conclusions and Future Work
References
A Refinement Repair Algorithm Based on Refinement Game for KMTS Models
1 Introduction
2 KMTS Refinement
2.1 Preserving Refinement Through KMTS Modifications
3 Refinement Game
4 Refinement Repair
4.1 Refinement Repair Algorithm
5 Conclusions and Future Works
References
Massive Open Online Courses and Monoids
1 Introduction
2 Examples, Semantics and Chomsky Classification
2.1 Learn Syntax: Formal and by Example
2.2 Learn Descriptions Are Partially-Ordered Monoids
3 Maude
4 Learn Maude Toolkit
4.1 Learn Descriptions as Rewrite Theories
4.2 Learn to Maude Transformer
4.3 Learn to HTML Transformer
5 Related Work
6 Conclusions
References
Model Checking
A Bounded Model Checker for Three-Valued Abstractions of Concurrent Software Systems
1 Introduction
2 Concurrent Software Systems
3 Three-Valued Bounded Model Checking
4 Propositional Logic Encoding
5 Extension to Fairness
6 Implementation
7 Related Work
8 Conclusion and Outlook
References
Model Checking Requirements
1 Introduction
2 Syntactic and Semantic Analyses of Requirements
3 CNL to NuSMV
3.1 Requirement Frame Pre-processing
3.2 Mapping Variables
3.3 Inferring the Types of the Variables
3.4 Building Transitions
3.5 NuSMV Code Generation
4 CNL to CTL
4.1 Natural-CTL
4.2 Implementation of a Syntax-Directed Translation
5 Case Study
5.1 Example: The Coffee Vending Machine
5.2 Retrieving the Variables
5.3 Inferring the Types of the Variables
5.4 Code Generation
5.5 Specifying Properties
6 Related Work
7 Conclusions
References
Refinement Verification of Sequence Diagrams Using CSP
1 Introduction
2 Background
2.1 Sequence Diagrams
2.2 CSP
3 Semantics and Refinement
3.1 Semantics
3.2 Refinement
4 Tool
5 Case Study
6 Related Work
7 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken