Livrables/Delivrables

Task1:  EXPLICIT SEMANTICS AND DOMAIN MODELLING. DEFINITION OF FORMAL MODELS FOR ONTOLOGIES

• T1.1_D1.1 (Formal model for Ontologies)
• T1.2_D1.2 (Event B encoding formal theories for ontologies)
• T1.3 _D1.3 (Building explicit semantic domain model : A Rodin Plugin and case studies I)
• T1.4 _D1.4 (Building explicit semantic domain model : A Rodin Plugin and case studies II)
• T1.5-D1.5 (Certification of proof contexts synthesis)

Task2:  EXPRESSING FORMAL DEVELOPMENTS IN IMPLICIT SEMANTICS.

• T2.1-2-D2.1 (Structuring Mechanisms for event- based models)
• T2.3-D2.2 (Annotating event-based models)

Task3: EXPLICIT AND IMPLICIT SEMANTICS HANDLING IN FORMAL DEVELOPMENTS

• T3.1-2-D3.1 (Formalising development operations in the presence of explicit semantics)
• T3.3-D3.2 (Properties handling: formalization and checking in the presence of explicit semantics)

Task4: MINING A DEVELOPMENT METHODOLOGY

• T4.1-D4.1 (Formal templates for integrating explicit knowledge in formal models)
• T4.2-D4.2 (Generic templates for properties)
• T4.3-D1.3 (under validation)
• T4.4-D4.4 (under validation)