Implicit and Explicit Semantics Integration in Proof Based Developments of Discrete Systems: Communications of Nii Shonan Meetings
暫譯: 離散系統的證明基礎開發中隱式與顯式語義整合：Nii Shonan 會議通訊

本書探討了由於在指定設計模型的正式技術中缺乏明確語義表達而引起的模型異質性減少機制。更精確地說，它突顯了在正式系統開發中處理隱式和顯式語義的進展，並討論了不同貢獻所表達的對隱式和顯式語義的不同觀點和看法。

本書基於2016年在湘南會議上針對此主題的討論，並包括參與者的貢獻，總結了他們對該問題的看法並提供解決方案。全書分為五個部分：領域建模、基於知識的建模、基於證明的建模、保證案例和基於細化的建模，並為正式方法、系統與軟體工程、領域知識建模、需求分析以及建模語言的顯式和隱式語義領域的研究者和實務工作者提供靈感。

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, CO₂ 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.

Yamine Ait Ameur 是圖盧茲國立理工學院的教授，也是計算機科學的 TCNRS IRIT 研究所的成員。他的研究主題包括 1) 驗證和確認的形式方法，2) 基於本體的建模和領域知識的明確化，以及 3) 應用領域：嵌入式系統、互動系統、語義網、網路物理系統及相關主題。他的研究活動有兩個主要特徵。一方面，通過使用基於細化和證明的形式建模技術（特別是使用 Event-B）來研究基本方面，並使用正式本體模型進行語義的明確化。另一方面，通過開發操作應用來解決實際問題，從而驗證所提出的方法。他的工作針對的應用領域包括航空電子學和鐵路系統中的嵌入式系統、工程、互動系統、二氧化碳捕集和網路物理系統。他是多篇發表於國際期刊和國際會議論文集的研究論文的作者，也是 ISO 13584 國際標準系列的主要編輯之一，該系列通常被稱為 PLib（零件庫），用於系統工程中的本體。

Shin Nakajima 是東京國立資訊學院的教授；同時擔任高等研究所的兼任教授；以及日本開放大學的訪問教授。他的研究主題包括形式方法、自動驗證、確保深度神經網絡軟體的質量、網路物理系統和軟體驅動的創新管理。他在這些主題上已出版六本書籍。

Dominique Méry 自 1993 年以來一直是洛林大學的計算機科學全職教授，並在信息技術學院 TELECOM Nancy 教學。他領導著 LORIA 的 MOSEL 研究小組，專注於形式方法及其應用，並與 CNRS、INRIA 和洛林大學合作。他曾是法國大學研究所 IUF 的初級成員（1995-2000），並且是 IFIP WG 1.3 規範基礎的成員。他目前的科學活動專注於使用細化的基於證明的分佈式算法開發，以及將網路物理系統建模為醫療設備。他的研究主要使用建模語言 B/Event-B 及相關平台。他曾主導 IMPEX ANR 項目，處理在基於證明的軟體系統開發中整合明確語義的問題。最後，他的研究探索了離散建模技術的範疇擴展，以處理混合系統的設計和建模。