Formal Methods: Foundations and Applications : 19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23-25, 2016, Proceedings / / edited by Leila Ribeiro, Thierry Lecomte

• Pubblicazione: Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016
• Edizione: 1st ed. 2016.
• Descrizione fisica: 1 online resource (X, 253 p. 62 illus.)
• Disciplina: 004.0151
• Soggetto topico: Software engineering; Computer science; Compilers (Computer programs); Computer simulation; Electronic data processing—Management; Machine theory; Software Engineering; Computer Science Logic and Foundations of Programming; Compilers and Interpreters; Computer Modelling; IT Operations; Formal Languages and Automata Theory
• Persona (resp. second.): RibeiroLeila; LecomteThierry
• Nota di contenuto: 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 Ł-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. ; 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.
• Sommario/riassunto: 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.
• Titolo autorizzato: Formal Methods: Foundations and Applications
• ISBN: 3-319-49815-0
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910483284603321
• Lo trovi qui: Univ. Federico II
• Serie: Programming and Software Engineering, . 2945-9168 ; ; 10090