Formal Methods: Foundations and Applications: 19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23-25, 2016, Proceedings (Lecture Notes in Computer Science Book 10090)

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. Preface 6 Organization 7 Contents 9 Invited Talks 11 Formal Model-Based Constraint Solving and Document Generation 12 1 Animation and Constraint Solving for B 12 2 Model-Based Constraint Solving 15 3 Model-Based Document Generation 16 4 A Portfolio of Constraint Solving Examples in B 18 4.1 Graph Colouring 18 4.2 Graph Isomorphism 18 4.3 N-Queens and Bishops 19 4.4 Golomb Ruler 21 4.5 Sudoku and Latin Squares 22 4.6 Coins Puzzle 24 5 External Data Sources and Data Validation 24 5.1 External Data Sources 24 5.2 Data Validation Example 25 6 Discussion 26 References 27 Formal Testing from Natural Language in an Industrial Context 30 1 Overview 30 2 Tools 32 2.1 Test Generation with TaRGeT 32 2.2 Test Automation with Zygon 33 3 Underlying Formalisms 36 3.1 Process Algebraic Approach to Test Generation 36 3.2 Contract Based Approach to Consistent Automation 40 4 Ongoing Work: Integrated Framework 44 References 46 Analysis and Verification 48 Application of Formal Methods to Verify Business Processes 49 1 Introduction 49 2 Theoretical Framework 50 2.1 Timed Automata (TA) 50 2.2 Business Process Model and Notation (BPMN) 52 2.3 Clocked Computation Tree Logic (CCTL) 54 3 BP-Task Model 55 4 Mapping Rules to Specify and Verify BPMN Models Using TA 55 5 CRM Application Example 60 5.1 CRM Task Model 62 5.2 CRM Properties 63 5.3 CRM Verification 64 6 Conclusion and Future Work 65 References 66 An Approach for Verifying Educational Robots 67 1 Introduction 67 2 Simulating Robot Programs 68 2.1 Overview of the Verification Approach 71 3 Formalising the Robot 71 3.1 Communicating Sequential Processes 71 3.2 Robot Formal Specification 73 4 Verifying Robot Programs 78 5 Integrating the Approach with Educational Tools 82 6 Conclusions 83 References 84 Verigraph: A System for Specification and Analysis of Graph Grammars 86 1 Introduction 86 2 Algebraic Graph Transformation 87 2.1 Example 88 2.2 Generalization and Other Approaches 89 3 Architecture Overview and Data Structures 90 4 Implemented Analysis Techniques 92 4.1 Critical Pair Analysis 93 4.2 Critical Sequence Analysis 95 4.3 Calculation of Concurrent Rules 96 4.4 State Space Exploration and Model Checking 97 4.5 Inter-Level Conflict Analysis 98 5 Related Work 99 5.1 AGG 99 5.2 GROOVE 99 5.3 Preliminary Performance Evaluation 99 6 Conclusions 101 References 101 Modeling and Logic 103 Modelling `Operation-Calls' in Event-B with Shared-Event Composition 104 1 Introduction 104 2 Event-B 105 3 An Overview of Event-B Components 106 4 Procedure-Style Interface Events 108 4.1 Procedural Interface Events 108 4.2 Translation of the Call 110 4.3 The Combined Event Representation 111 5 Function-Style Interface Events for Use in Expressions 111 5.1 Functional Interface Events 111 5.2 Translation of the Call 112 5.3 The Combined Event Representation 113 6 Discussion and Related Work 114 6.1 A Comparison with the Modularisation Approach -- in More Detail 115 7 Conclusions 116 References 117 Algebraic Foundations for Specification Refinements 119 1 Introduction 119 2 Preliminaries 120 3 A Category of Refinements 122 3.1 Heterogeneous Refinements 130 4 Data Refinement 131 5 Related Work and Conclusions 133 References 134 On Interval Dynamic Logic 136 1 Introduction 136 2 An Ł-Fuzzy Dynamic Logic 138 2.1 The Łukasiewicz Action Lattice 138 2.2 The Ł-Fuzzy Dynamic Logic 140 3 Ł-Interval Algebra 143 3.1 On the Interval Łukasiewicz Lattice 144 4 The Price 147 5 Conclusion and Further Work 148 References 149 An Evolutionary Approach to Translate Operational Specifications into Declarative Specifications 152 1 Introduction 152 2 A Motivating Example 154 3 An Evolutionary Algorithm for Learning Declarative Specifications 157 3.1 Genes and Chromosomes to Represent Candidate Specifications 158 3.2 Fitness of Candidate Specifications 159 3.3 Overall Structure of the Genetic Algorithm for Learning Specifications 160 4 Validation 161 4.1 Assessment 163 5 Related Work 164 6 Conclusions and Future Work 165 References 166 A Refinement Repair Algorithm Based on Refinement Game for KMTS Models 168 1 Introduction 168 2 KMTS Refinement 169 2.1 Preserving Refinement Through KMTS Modifications 172 3 Refinement Game 174 4 Refinement Repair 179 4.1 Refinement Repair Algorithm 180 5 Conclusions and Future Works 184 References 185 Massive Open Online Courses and Monoids 186 1 Introduction 186 2 Examples, Semantics and Chomsky Classification 188 2.1 Learn Syntax: Formal and by Example 188 2.2 Learn Descriptions Are Partially-Ordered Monoids 190 3 Maude 191 4 Learn Maude Toolkit 194 4.1 Learn Descriptions as Rewrite Theories 195 4.2 Learn to Maude Transformer 197 4.3 Learn to HTML Transformer 199 5 Related Work 200 6 Conclusions 201 References 201 Model Checking 203 A Bounded Model Checker for Three-Valued Abstractions of Concurrent Software Systems 204 1 Introduction 204 2 Concurrent Software Systems 205 3 Three-Valued Bounded Model Checking 208 4 Propositional Logic Encoding 211 5 Extension to Fairness 216 6 Implementation 217 7 Related Work 219 8 Conclusion and Outlook 220 References 220 Model Checking Requirements 222 1 Introduction 222 2 Syntactic and Semantic Analyses of Requirements 224 3 CNL to NuSMV 225 3.1 Requirement Frame Pre-processing 226 3.2 Mapping Variables 226 3.3 Inferring the Types of the Variables 226 3.4 Building Transitions 228 3.5 NuSMV Code Generation 228 4 CNL to CTL 229 4.1 Natural-CTL 229 4.2 Implementation of a Syntax-Directed Translation 230 5 Case Study 231 5.1 Example: The Coffee Vending Machine 231 5.2 Retrieving the Variables 232 5.3 Inferring the Types of the Variables 233 5.4 Code Generation 234 5.5 Specifying Properties 234 6 Related Work 236 7 Conclusions 237 References 238 Refinement Verification of Sequence Diagrams Using CSP 240 1 Introduction 240 2 Background 241 2.1 Sequence Diagrams 241 2.2 CSP 243 3 Semantics and Refinement 243 3.1 Semantics 244 3.2 Refinement 245 4 Tool 250 5 Case Study 252 6 Related Work 253 7 Conclusion 255 References 256 Author Index 258 Front Matter....Pages I-X Front Matter....Pages 1-1 Formal Model-Based Constraint Solving and Document Generation....Pages 3-20 Formal Testing from Natural Language in an Industrial Context....Pages 21-38 Front Matter....Pages 39-39 Application of Formal Methods to Verify Business Processes....Pages 41-58 An Approach for Verifying Educational Robots....Pages 59-77 Verigraph: A System for Specification and Analysis of Graph Grammars....Pages 78-94 Front Matter....Pages 95-95 Modelling ‘Operation-Calls’ in Event-B with Shared-Event Composition....Pages 97-111 Algebraic Foundations for Specification Refinements....Pages 112-128 On Interval Dynamic Logic....Pages 129-144 An Evolutionary Approach to Translate Operational Specifications into Declarative Specifications....Pages 145-160 A Refinement Repair Algorithm Based on Refinement Game for KMTS Models....Pages 161-178 Massive Open Online Courses and Monoids....Pages 179-195 Front Matter....Pages 197-197 A Bounded Model Checker for Three-Valued Abstractions of Concurrent Software Systems....Pages 199-216 Model Checking Requirements....Pages 217-234 Refinement Verification of Sequence Diagrams Using CSP....Pages 235-252 Back Matter....Pages 253-253