Read While You Wait - Get immediate ebook access, if available*, when you order a print book

Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems

Communications of NII Shonan Meetings

Editors: Ait-Ameur, Yamine, Nakajima, Shin, Méry, Dominique (Eds.)

Free Preview
  • Provides an introduction to formal techniques for domain knowledge and formal system modelling
  • Summarises the latest studies in handling explicit and implicit semantics in formal system development
  • Reviews various approaches and lessons learnt in formal domain knowledge modelling in formal system formal developments
see more benefits

Buy this book

eBook 93,08 €
price for Spain (gross)
  • ISBN 978-981-15-5054-6
  • Digitally watermarked, DRM-free
  • Included format: PDF, EPUB
  • ebooks can be used on all reading devices
  • Immediate eBook download after purchase
Hardcover 114,39 €
price for Spain (gross)
About this book

This book addresses mechanisms for reducing model heterogeneity induced by the absence of explicit semantics expression in the formal techniques used to specify design models. More precisely, it highlights the advances in handling both implicit and explicit semantics in formal system developments, and discusses different contributions expressing different views and perceptions on the implicit and explicit semantics.

The book is based on the discussions at the Shonan meeting on this topic held in 2016, and includes contributions from the participants summarising their perspectives on the problem and offering solutions. Divided into 5 parts: domain modelling, knowledge-based modelling, proof-based modelling, assurance cases, and refinement-based modelling, and offers inspiration for researchers and practitioners in the fields of formal methods, system and software engineering, domain knowledge modelling, requirement analysis, and explicit and implicit semantics of modelling languages.

About the authors

Yamine Ait Ameur is a professor at Toulouse National Polytechnique Institute and a member of the TCNRS IRIT Research Institute in Computer Science. His research topics concern 1) Formal methods for validation and verification, 2) Ontology-based modelling and domain knowledge explicitation, and 3) Application domains: embedded systems, interactive systems, semantic web, cyber-physical systems, and related topics. Two main important aspects characterize his research activities. On the one hand the fundamental aspects are studied through the use of formal modelling techniques based on refinement and proof (in particular, using Event-B), explicit formalisation of semantics employing formal ontology models. On the other hand, practical aspects are addressed through the development of operational applications, allowing validation of the proposed approaches. Embedded systems in avionics and railway systems, engineering, interactive systems, CO2 capture, and cyber physical systems are some of the application domains targeted by his work. He is the author of several research papers published in international journals and in the proceedings of international conferences. He is one of the main editors of the ISO 13584 International Standard Series, commonly known as PLib (Parts Libraries) for ontologies in system engineering.

Shin Nakajima is a professor at the National Institute of Informatics, Tokyo; an adjunct professor at the Graduate University for Advanced Studies; and a visiting professor at the Open University of Japan. His research topics concern formal methods, automated verification, assuring the quality of deep neural networks software, cyber-physical systems, and software-enabled innovation management. He has authored six books on those subjects.

Dominique Méry has been a full professor of computing science at the University of Lorraine since 1993 and is teaching in the School of Engineering in Information Technology TELECOM Nancy.  He is leading the research group MOSEL on formal methods and applications in LORIA, jointly with CNRS, INRIA, and the University of Lorraine. He has been a junior member of the Institut Universitaire de France IUF (1995–2000) and is a member of the IFIP WG 1.3 on foundations of specifications.  His current scientific activities a focus on proof-based development of distributed algorithms using the refinement, as well as modelling, of cyber physical systems as medical devices. His research uses mainly the modelling language B/Event-B and related platforms. He has led the IMPEX ANR project dealing with the integration of the explicit semantics in the proof-based development of software systems. Finally, his research explores the extension of the scope of discrete modelling techniques to handle the design and modelling of hybrid systems.

Table of contents (15 chapters)

Table of contents (15 chapters)
  • Modelling an E-Voting Domain for the Formal Development of a Software Product Line: When the Implicit Should Be Made Explicit

    Pages 3-18

    Gibson, J. Paul (et al.)

  • Domain-Specific Developments Using Rodin Theories

    Pages 19-37

    Hoang, Thai Son (et al.)

  • Integrating Domain Modeling Within a Formal Requirements Engineering Method

    Pages 39-58

    Tueno, Steve (et al.)

  • Operations over Lightweight Ontologies and Their Implementation

    Pages 61-82

    Casanova, Marco A. (et al.)

  • Formal Ontological Analysis for Medical Protocols

    Pages 83-107

    Singh, Neeraj Kumar (et al.)

Buy this book

eBook 93,08 €
price for Spain (gross)
  • ISBN 978-981-15-5054-6
  • Digitally watermarked, DRM-free
  • Included format: PDF, EPUB
  • ebooks can be used on all reading devices
  • Immediate eBook download after purchase
Hardcover 114,39 €
price for Spain (gross)
Loading...

Recommended for you

Loading...

Bibliographic Information

Bibliographic Information
Book Title
Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems
Book Subtitle
Communications of NII Shonan Meetings
Editors
  • Yamine Ait-Ameur
  • Shin Nakajima
  • Dominique Méry
Copyright
2021
Publisher
Springer Singapore
Copyright Holder
Springer Nature Singapore Pte Ltd.
eBook ISBN
978-981-15-5054-6
DOI
10.1007/978-981-15-5054-6
Hardcover ISBN
978-981-15-5053-9
Edition Number
1
Number of Pages
XII, 346
Number of Illustrations
109 b/w illustrations, 29 illustrations in colour
Topics

*immediately available upon purchase as print book shipments may be delayed due to the COVID-19 crisis. ebook access is temporary and does not include ownership of the ebook. Only valid for books with an ebook version. Springer Reference Works and instructor copies are not included.