Skip to main content

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

Communications of NII Shonan Meetings

  • Book
  • © 2021

Overview

  • 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

This is a preview of subscription content, log in via an institution to check access.

Access this book

eBook USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (15 chapters)

  1. Domain Modelling

  2. Knowledge Based Modelling

  3. Proof Based Modelling

  4. Assurance Cases

  5. Refinement Based Modelling

Keywords

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.

Editors and Affiliations

  • Department of Computing and Applied Mathematics, IRIT/INPT-ENSEEIHT, Toulouse, France

    Yamine Ait-Ameur

  • National Institute of Informatics, Tokyo, Japan

    Shin Nakajima

  • Telecom Nancy, University of Lorraine, Vandœuvre-lès-Nancy, France

    Dominique Méry

About the editors

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.

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

  • DOI: https://doi.org/10.1007/978-981-15-5054-6

  • Publisher: Springer Singapore

  • eBook Packages: Computer Science, Computer Science (R0)

  • Copyright Information: Springer Nature Singapore Pte Ltd. 2021

  • Hardcover ISBN: 978-981-15-5053-9Published: 28 July 2020

  • Softcover ISBN: 978-981-15-5056-0Published: 29 July 2021

  • eBook ISBN: 978-981-15-5054-6Published: 27 July 2020

  • Edition Number: 1

  • Number of Pages: XII, 346

  • Number of Illustrations: 109 b/w illustrations, 29 illustrations in colour

  • Topics: Software Engineering, Mathematical Logic and Foundations

Publish with us