ebook img

Software Engineering and Formal Methods: SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS, Grenoble, France, September 1-2, 2014, Revised Selected Papers PDF

426 Pages·2015·41.12 MB·English
Save to my drive
Quick download
Download
Most books are stored in the elastic cloud where traffic is expensive. For this reason, we have a limit on daily download.

Preview Software Engineering and Formal Methods: SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS, Grenoble, France, September 1-2, 2014, Revised Selected Papers

Carlos Canal Akram Idani (Eds.) 8 3 Software Engineering 9 8 S C and Formal Methods N L SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS Grenoble, France, September 1–2, 2014, Revised Selected Papers 123 Lecture Notes in Computer Science 8938 Commenced Publication in 1973 Founding and Former Series Editors: Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen Editorial Board David Hutchison Lancaster University, Lancaster, UK Takeo Kanade Carnegie Mellon University, Pittsburgh, PA, USA Josef Kittler University of Surrey, Guildford, UK Jon M. Kleinberg Cornell University, Ithaca, NY, USA Friedemann Mattern ETH Zurich, Zürich, Switzerland John C. Mitchell Stanford University, Stanford, CA, USA Moni Naor Weizmann Institute of Science, Rehovot, Israel C. Pandu Rangan Indian Institute of Technology, Madras, India Bernhard Steffen TU Dortmund University, Dortmund, Germany Demetri Terzopoulos University of California, Los Angeles, CA, USA Doug Tygar University of California, Berkeley, CA, USA Gerhard Weikum Max Planck Institute for Informatics, Saarbrücken, Germany More information about this series at http://www.springer.com/series/7408 Carlos Canal Akram Idani (Eds.) (cid:129) Software Engineering and Formal Methods SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS – Grenoble, France, September 1 2, 2014 Revised Selected Papers 123 Editors CarlosCanal AkramIdani Universityof Malaga LIGLab Malaga Saint Martind’HèresCedex Spain France ISSN 0302-9743 ISSN 1611-3349 (electronic) Lecture Notesin ComputerScience ISBN 978-3-319-15200-4 ISBN 978-3-319-15201-1 (eBook) DOI 10.1007/978-3-319-15201-1 LibraryofCongressControlNumber:2014960220 LNCSSublibrary:SL2–ProgrammingandSoftwareEngineering SpringerChamHeidelbergNewYorkDordrechtLondon ©SpringerInternationalPublishingSwitzerland2015 Thisworkissubjecttocopyright.AllrightsarereservedbythePublisher,whetherthewholeorpartofthe material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storageandretrieval,electronicadaptation,computersoftware,orbysimilarordissimilarmethodologynow knownorhereafterdeveloped. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Thepublisher,theauthorsandtheeditorsaresafetoassumethattheadviceandinformationinthisbookare believedtobetrueandaccurateatthedateofpublication.Neitherthepublishernortheauthorsortheeditors give a warranty, express or implied, with respect to the material contained herein or for any errors or omissionsthatmayhavebeenmade. Printedonacid-freepaper SpringerInternationalPublishingAGSwitzerlandispartofSpringerScience+BusinessMedia (www.springer.com) Preface Thisvolumecontainsthetechnicalpaperspresentedinthefivehigh-qualityworkshops associatedtoSEFM2014(12thInternationalConferenceonSoftwareEngineeringand FormalMethods,heldinGrenoble,September1–5,2014).SEFM2014wasorganized by Inria and supported by Grenoble INP, Joseph Fourier University, LIG, and CNRS. SEFM2014broughttogetherpractitionersandresearchersfromacademia,industry, and government to advance the state of the art in formal methods, to facilitate their uptake in the software industry, and to encourage their integration with practical engineering methods. Satellite workshops provided further opportunities for collabo- rating and exchanging ideas about specific topics of Formal Methods and Software Engineering, from conceptual to practical aspects. The workshops focused on specific topics in the Software Engineering and Formal Methods related domains: the First Workshop on Human-Oriented Formal Methods – FromReadabilitytoAutomation(HOFM2014),theThirdInternationalSymposiumon Modeling and Knowledge Management Applications – Systems and Domains (MoKMaSD 2014), the Eighth International Workshop on Foundations and Tech- niquesforOpenSourceSoftwareCertification(OpenCert2014),theFirstWorkshopon Safety and Formal Methods (SaFoMe 2014), and the Fourth Workshop on Formal Methods in the Development of Software (WS-FMDS 2014). The review and the selectionprocesswasperformedrigorously,witheachpaperbeingreviewedbyatleast three Program Committee (PC) members. A brief description of each workshop follows, written by their organizers. For each of the workshops at SEFM 2014, we thank the organizers for these interesting topics and resulting talks. We also thank the paper contributors to these workshops and those who attended them. We would like to extend our thanks toallkeynotespeakersfortheirsupportandexcellentpresentations,andalso,members of each workshop’s Program Committee. September 2014 Carlos Canal Akram Idani HOFM Organizers’ Message While designing and applying formal methods, computer scientists have dominantly focusedontwofactorsonly:first,amethodmustbepreciseandsound,andsecondly, itmustbemathematically concise and aesthetic.Other importantcharacteristicssuch as simplicity, learnability, readability, memorability, ease of use and communication or, even support for integrating tools into larger development tool chains are ignored toooften.Thesenonfunctionalproperties,however,arekeyattributesofusabilityand user satisfaction. If usability is compromised, methods are not fit for the purpose of documenting, reproducing, and communicating key design and realization decisions, or analysis results, especially when these need to communicate or mediate between expertise in different disciplines, different tool chains, or across technological or organizationalboundaries.Forthesereasons,manyengineersandpractitionerslargely reject formal methods and formal specification languages as “too hard to understand and use in practice” while admitting that they are powerful and precise. With increasing computing power and its consequent automation capabilities, the research and development community, however, is slowly but definitely focusing on usability in combination with automation. Moreover, practitioners across numerous domains are increasingly interested in formal domain-specific modeling, simulation, and validation, whether in application areas of energy, robotics, health, biology, climate,andsustainabledevelopment,or,forspecifictechnologiesofimportancesuch asdataanalyticsanduserinterfacespecificationforanexponentiallygrowingnumber of handheld or wearable devices. While there are many applications of formal methods to analyze human-machine interaction and to construct user interfaces, the fieldofapplicationofhumanfactorstotheanalysisandtotheoptimizationofformal methods area is almost unexplored. The HOFM workshop was held on September 1, 2014 in Grenoble, France. This internationalworkshopwasaffiliatedtothe12thInternationalConferenceonSoftware Engineering and Formal Methods (SEFM). The goal of the HOFM (Human-Oriented Formal Methods) workshop was to bring together researchers, engineers, and practitioners from academia and industry to baseline the state of the art in this increasinglyimportantdomain.Everysubmittedpaperwasreviewedbyatleastthree Program Committee members, four regular papers were accepted for presentation at HOFM 2014. An introduction to the first HOFM workshop was given by Maria Spichkova on “Human-Oriented Formal Methods: Human Factors + Formal Methods.” The program of the workshop was enriched by two keynote talks: – Arkady Zaslavsky, CSIRO, Australia, “Internet of Things: New Dimensions of Modelling, Usability and Human-Computer Interaction” – MartinGlinz,UniversityofZurich,Switzerland,“AdvantagesandPitfallsofFormal or Formalizable Graphic Requirements Models” The HOFM 2014 pre-proceedings, which include all papers presented at the workshop, are available online at the workshop site http://hofm2014.wordpress.com. VIII HOFM Organizers’ Message AllauthorsoftheHOFMworkshopwereinvitedtosubmitextendedversionsoftheir papers, taking into account discussions made during the workshop. We would like to thank all authors who contributed to HOFM 2014 as well as all attendeesto the workshop. We hope that the attendeesfound the program relevantto theirinterestsandinspiring.WealsothanktheProgramCommitteemembersfortheir supportand considered reviews,and the SEFM workshop chairs and local organizers for their help. Maria Spichkova Heinz W. Schmidt Program Committee Katherine Blashki Noroff University College, Norway Manfred Broy Technical University of Munich, Germany Jan Carlson Mälardalen University, Sweden Pedro Isaas Universidade Aberta, Portugal Lalchandani Jayprakash IIIT Bangalore, India Margaret Hamilton RMIT University, Australia Peter Herrmann NTNU Trondheim, Norway Tim Miller The University of Melbourne, Australia Srini Ramaswamy ABB Bangalore, India Daniel Ratiu Siemens AG, Germany Bernhard Schätz fortiss GmbH, Germany Heinz W. Schmidt (Chair) RMIT University, Australia Carol Smidts Ohio State University, USA Maria Spichkova (Chair) RMIT University, Australia Judith Stafford University of Colorado, USA SaFoMe Organizers’ Message Theenhancementofqualityofservice(QoS)andthereductionoftheriskoffatalities andinjuriesofstrategicindustrialproductsisarealneedinmanydomains,including for instance automotive, avionics, and rail. To achieve this, there is a need for cost- efficient processes and methods supporting the development and operation of safety enabling embedded systems. Among several approaches, Component-Based Development (CBD) has emerged as suitable to improve both the reuse and maintainability of systems. Many CBD techniquesusetheconceptofacontract,whichdescribeswhatacomponentinterface provides and what it expects from other components. During system composition contracts are compared to determine system compatibility. The majority of these works has concentrated on the functional properties of systems. Much less work has been devoted to apply CBD while dealing with nonfunctional properties, including dependability properties such as safety, reliability, performance, and availability. Formal methods have traditionally been advocated for improving the reliability of safety-relevant systems. The First International Workshop on Safety and Formal Methods, SaFoMe2014,whichwasheldinGrenoble,France,onSeptember1,2014, aimed at providing a forum for people from academia and industry to communicate theirlatestresultsontheoreticaladvances,industrialcasestudies,andlessonslearned in the application of formal methods to safety certification, verification, and/or validation in (but not limited to) component-based systems. Papers submitted to SaFoMe 2014 were carefully reviewed by at least three membersoftheProgramCommittee.Fromninesubmissions,fivepaperswerefinally selectedtodiscussthefollowingtopics:survivability,diagnosis,verificationofsafety contracts,andformalizationofbehavioralpatternsandsharedresources.Prof.Dr.Jan Jürgens from TU Dortmund and Fraunhofer ISST gave an invited talk on Security CertificationinthePresenceofEvolution:Modelsvs.Code.ARoundTablewasheld at the end of the workshop where current challenges in industrial application of FormalMethodsinthesafetycontextwereactivelydiscussedbytheattendees,which consistedofpeoplebothfromacademiaandindustry.Theconclusionwasthatweare still far from applying formal methods to deal with safety concerns in industrial contexts,sincetherearetoomanymodelinglanguagesandtoolsthatpartiallyanalyze safety concerns while considering the evolving requirements. Several people contributed to the success of SaFoMe 2014. We would like to express our gratitude to all members of the Program Committee for their efforts and commitment. The SEFM workshop’s organizers deserve special thanks for their dedicationandgoodwork,whichclearlymadeourorganizationtaskseasier.Wealso thank the nSafeCer project (EU ARTEMIS Joint Undertaking under grant agreement no. 295373) for their support. Finally, thanks to the authors and attendees for their passion and interest. X SaFoMe Organizers’ Message Program Co-chairs Hans Hansson Clara Benac Earle Organization Committee Elena Gómez-Martínez Ricardo J. Rodríguez Catia Trubiani Program Committee Clara Benac Earle Universidad Politécnica de Madrid, Spain Simona Bernardi Centro Universitario de la Defensa, Universidad de Zaragoza, Spain Jan Carlson Mälardalen University, Sweden David Garcia-Rosado Universidad de Castilla-La Mancha, Spain Christophe Gaston Institut CARNOT CEA LIST, France Elena Gómez-Martínez Universidad Politécnica de Madrid, Spain Hans Hansson Mälardalen University, Sweden José Merseguer Universidad de Zaragoza, Spain Sasikumar Punnekkat Mälardalen University, Sweden Nicolas Rapin Institut CARNOT CEA LIST, France Ricardo J. Rodríguez Universidad de León, Spain Fernando Rosa-Velardo Universidad Complutense de Madrid, Spain Stefano Tonetta Fondazione Bruno Kessler, Italy Catia Trubiani Gran Sasso Science Institute, Italy Xavier Zeitoun Institut CARNOT CEA LIST, France

See more

The list of books you might like

Most books are stored in the elastic cloud where traffic is expensive. For this reason, we have a limit on daily download.