Software engineering and formal methods : SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS, Grenoble, France, September 1-2, 2014 : revised selected papers

This Book Constitutes Revised Selected Papers From The Workshops Collocated With The Sefm 2014 Conference On Software Engineering And Formal Methods, Held In Grenoble, France, In September 2014. The 26 Papers Included In This Volume Were Carefully Reviewed And Selected From 49 Submissions. They Are From The Following Workshops: The 1st Workshop On Human-oriented Formal Methods - From Readability To Automation, Hofm 2014, The 3rd International Symposium On Modelling And Knowledge Management Applications - Systems And Domains, Mokmasd 2014, The 8th International Workshop On Foundations And Techniques For Open Source Software Certification, Open Cert 2014, The 1st Workshop On Safety And Formal Methods, Safome 2014, And The 4th Workshop On Formal Methods In The Development Of Software, Ws-fmds 2014. Invited Papers -- Reasoning About Separation Using Abstraction And Reification -- An Interface Theory For The Internet Of Things -- Program Verification -- Learning Assertions To Verify Linked-list Programs -- Verifying Protocol Implementations By Augmenting Existing Cryptographic Libraries With Specifications -- Specification And Verification Of Atomic Operations In Gpgpu Programs -- History-based Verification Of Functional Behaviour Of Concurrent Programs -- Investigating Instrumentation Techniques For Esb Runtime Verification -- Towards Domain Refinement For Uml/ocl Bounded Verification -- Testing -- Efficient Testing Of Different Loop Paths -- Model-based Robustness Testing In Event-b Using Mutation -- On The Testability Of Properties Patterns -- Certification -- Speed Up Configurable Certificate Validation By Certificate Reduction And Partitioning -- Formal Analysis Of Proactive, Distributed Routing -- Certification Of Distributed Algorithms Solving Problems With Optimal Substructure -- Formal Specification And Proof -- From Failure To Proof: The Prob Disprover For B And Event-b -- Formalizing A Secure Foreign Function Interface -- A Formal Study Of Backward Compatible Dynamic Software Updates -- Testing And Model Checking -- Memory Management Test-case Generation Of C Programs Using Bounded Model Checking -- Techniques For Memory-efficient Model Checking Of C And C++ Code -- Nat2test Tool: From Natural Language Requirements To Test Cases Based On Csp -- Planning -- Task Planning Of Cyber-human Systems -- Generating None-plans In Order To Find Plans -- Modelling And Model Transformation Twitlang(er): Interactions Modeling Language (and Interpreter) For Twitter -- From Featured Transition Systems To Modal Transition Systems With Variability Constraints -- An Extensible Operational Semantics For Uml Activity Diagrams. Edited By Carlos Canal, Akram Idani. Front Matter....Pages I-XXVII Front Matter....Pages 1-1 A Usability Evaluation of Interactive Theorem Provers Using Focus Groups....Pages 3-19 An Approach for Creating Domain Specific Visualisations of CSP Models....Pages 20-35 Using Z in the Development and Maintenance of Computational Models of Real-World Systems....Pages 36-53 When a Formal Model Rhymes with a Graphical Notation....Pages 54-68 Front Matter....Pages 69-69 On a Process Algebraic Representation of Sequence Diagrams....Pages 71-85 Modelling and Verification of Survivability Requirements for Critical Systems....Pages 86-100 Model-Based Verification of Safety Contracts....Pages 101-115 A Testing-Based Approach to Ensure the Safety of Shared Resource Concurrent Systems....Pages 116-130 A Contracts-Based Framework for Systems Modeling and Embedded Diagnostics....Pages 131-143 Front Matter....Pages 145-145 Modelling and Verifying Smell-Free Architectures with the Archery Language....Pages 147-163 OntoLiFLOSS: Ontology for Learning Processes in FLOSS Communities....Pages 164-181 Process Mining Event Logs from FLOSS Data: State of the Art and Perspectives....Pages 182-198 Front Matter....Pages 199-199 A Latent Representation Model for Sentiment Analysis in Heterogeneous Social Networks....Pages 201-213 Use of Mobile Phone Data to Estimate Visitors Mobility Flows....Pages 214-226 An Abstract State Machine (ASM) Representation of Learning Process in FLOSS Communities....Pages 227-242 A Mathematical Model for Assessing KRAS Mutation Effect on Monoclonal Antibody Treatment of Colorectal Cancer....Pages 243-258 Sea-Scale Agent-Based Simulator of Solea solea in the Adriatic Sea....Pages 259-275 Research Challenges in Modelling Ecosystems....Pages 276-293 Retrieving Points of Interest from Human Systematic Movements....Pages 294-308 Front Matter....Pages 309-309 Path-Sensitive Race Detection with Partial Order Reduced Symbolic Execution....Pages 311-322 Front Matter....Pages 309-309 Phase-Type Approximations for Non-Markovian Systems: A Case Study....Pages 323-334 Quantitative Anonymity Evaluation of Voting Protocols....Pages 335-349 Scalable Verification of Markov Decision Processes....Pages 350-362 Towards Synthesis of Attack Trees for Supporting Computer-Aided Risk Analysis....Pages 363-375 On Generation of Context-Abstract Plans....Pages 376-388 A Coloured Petri Net Approach to Model and Analyse Stateful Workflows Based on WS-BPEL and WSRF....Pages 389-404 Back Matter....Pages 405-405