Formal Methods: Foundations and Applications
19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23-25, 2016, Proceedings
Published on 12. November 2016
X, 253 pages
978-3-319-49815-7 (ISBN)
Description
This book constitutes the refereed proceedings of the 19th Brazilian Symposium on Formal Methods, SBMF 2016, which took place in Natal, Brazil, in November 2016.
The 12 papers presented together with two invited talks were carefully reviewed and selected from 22 submissions. They are organized in the following topical sections: analysis and verification; modeling and logic; and model checking.
The 12 papers presented together with two invited talks were carefully reviewed and selected from 22 submissions. They are organized in the following topical sections: analysis and verification; modeling and logic; and model checking.
More details
Series
Edition
1st ed. 2016
Language
English
Place of publication
Cham
Switzerland
Publishing group
Springer International Publishing
Product notice
Reflowable
Illustrations
X, 253 p. 62 illus.
File size
19,59 MB
ISBN-13
978-3-319-49815-7 (9783319498157)
DOI
10.1007/978-3-319-49815-7
Schweitzer Classification
Other editions
Additional editions
Leila Ribeiro | Thierry Lecomte
Formal Methods: Foundations and Applications
19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23-25, 2016, Proceedings
Book
11/2016
Springer
€53.49
Shipment within 10-15 days
Content
- 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
