Showing 1–2 of 2 results for author: Ameur, Y A

A Complete Fragment of LTL(EB)

Authors: Flavio Ferrarotti, Peter Rivière, Klaus-Dieter Schewe, Neeraj Kumar Singh, Yamine Aït Ameur

Abstract: The verification of liveness conditions is an important aspect of state-based rigorous methods. This article investigates this problem in a fragment $\square$LTL of the logic LTL(EB), the integration of the UNTIL-fragment of Pnueli's linear time temporal logic (LTL) and the logic of Event-B, in which the most commonly used liveness conditions can be expressed. For this fragment a sound set of deri… ▽ More The verification of liveness conditions is an important aspect of state-based rigorous methods. This article investigates this problem in a fragment $\square$LTL of the logic LTL(EB), the integration of the UNTIL-fragment of Pnueli's linear time temporal logic (LTL) and the logic of Event-B, in which the most commonly used liveness conditions can be expressed. For this fragment a sound set of derivation rules is developed, which is also complete under mild restrictions for Event-B machines. △ Less

Submitted 30 January, 2024; originally announced January 2024.

Comments: 22 pages

MSC Class: 68Q60; 68N30

Formal Modelling of Ontologies : An Event-B based Approach Using the Rodin Platform

Authors: Yamine Ait Ameur, Idir Ait Sadoune, Kahina Hacid, Linda Mohand Oussaid

Abstract: This paper reports on the results of the French ANR IMPEX research project dealing with making explicit domain knowledge in design models. Ontologies are formalised as theories with sets, axioms, theorems and reasoning rules. They are integrated to design models through an annotation mechanism. Event-B has been chosen as the ground formal modelling technique for all our developments. In this paper… ▽ More This paper reports on the results of the French ANR IMPEX research project dealing with making explicit domain knowledge in design models. Ontologies are formalised as theories with sets, axioms, theorems and reasoning rules. They are integrated to design models through an annotation mechanism. Event-B has been chosen as the ground formal modelling technique for all our developments. In this paper, we particularly describe how ontologies are formalised as Event-B theories. △ Less

Submitted 14 May, 2018; originally announced May 2018.

Comments: In Proceedings IMPEX 2017 and FM&MDD 2017, arXiv:1805.04636

Journal ref: EPTCS 271, 2018, pp. 24-33