LEADER 08989nam 22007935 450 001 9910483284603321 005 20251226200504.0 010 $a3-319-49815-0 024 7 $a10.1007/978-3-319-49815-7 035 $a(CKB)3710000000981125 035 $a(DE-He213)978-3-319-49815-7 035 $a(MiAaPQ)EBC6303125 035 $a(MiAaPQ)EBC5610590 035 $a(Au-PeEL)EBL5610590 035 $a(OCoLC)1079007416 035 $a(PPN)197137326 035 $a(EXLCZ)993710000000981125 100 $a20161112d2016 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aFormal Methods: Foundations and Applications $e19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23-25, 2016, Proceedings /$fedited by Leila Ribeiro, Thierry Lecomte 205 $a1st ed. 2016. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2016. 215 $a1 online resource (X, 253 p. 62 illus.) 225 1 $aProgramming and Software Engineering,$x2945-9168 ;$v10090 311 08$a3-319-49814-2 327 $aIntro -- 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. 327 $a2 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 ?-Fuzzy Dynamic Logic -- 2.1 The ?ukasiewicz Action Lattice -- 2.2 The ?-Fuzzy Dynamic Logic -- 3 ?-Interval Algebra -- 3.1 On the Interval ?ukasiewicz 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. 327 $a3.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. 327 $aRefinement 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. 330 $aThis 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. 410 0$aProgramming and Software Engineering,$x2945-9168 ;$v10090 606 $aSoftware engineering 606 $aComputer science 606 $aCompilers (Computer programs) 606 $aComputer simulation 606 $aElectronic data processing$xManagement 606 $aMachine theory 606 $aSoftware Engineering 606 $aComputer Science Logic and Foundations of Programming 606 $aCompilers and Interpreters 606 $aComputer Modelling 606 $aIT Operations 606 $aFormal Languages and Automata Theory 615 0$aSoftware engineering. 615 0$aComputer science. 615 0$aCompilers (Computer programs). 615 0$aComputer simulation. 615 0$aElectronic data processing$xManagement. 615 0$aMachine theory. 615 14$aSoftware Engineering. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aCompilers and Interpreters. 615 24$aComputer Modelling. 615 24$aIT Operations. 615 24$aFormal Languages and Automata Theory. 676 $a004.0151 702 $aRibeiro$b Leila$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aLecomte$b Thierry$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483284603321 996 $aFormal Methods: Foundations and Applications$9773789 997 $aUNINA