Integrating Domain Modeling Within a Formal Requirements Engineering Method

Steve Tueno; Régine Laleau; Amel Mammar; Marc Frappier

doi:10.1007/978-981-15-5054-6_3

Integrating Domain Modeling Within a Formal Requirements Engineering Method

Steve Tueno
, Régine Laleau
, Amel Mammar
, Marc Frappier

Université de PARIS XII
Université de Sherbrooke

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

Abstract

One way to build safe critical systems is to formally model the requirements formulated by stakeholders and to ensure their consistency with respect to domain properties. This paper describes a metamodel for a domain modeling language built from OWL and PLIB. The language is part of the SysML/KAOS requirements engineering method which also includes a goal modeling language. The formal semantics of SysML/KAOS models is specified, verified, and validated using the Event-B method. Goal models provide machines and events of the Event-B specification while domain models provide its structural part (sets and constants with their properties and variables with their invariant). Our proposal is illustrated with a case study dealing with the specification of a localization component for an autonomous vehicle.

Original language	English
Title of host publication	Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems
Subtitle of host publication	Communications of NII Shonan Meetings
Publisher	Springer Singapore
Pages	39-58
Number of pages	20
ISBN (Electronic)	9789811550546
ISBN (Print)	9789811550539
DOIs	https://doi.org/10.1007/978-981-15-5054-6_3
Publication status	Published - 1 Jan 2020

Access to Document

10.1007/978-981-15-5054-6_3

Cite this

@inbook{c331a9a8b4e14861961142b886780fe4,

title = "Integrating Domain Modeling Within a Formal Requirements Engineering Method",

abstract = "One way to build safe critical systems is to formally model the requirements formulated by stakeholders and to ensure their consistency with respect to domain properties. This paper describes a metamodel for a domain modeling language built from OWL and PLIB. The language is part of the SysML/KAOS requirements engineering method which also includes a goal modeling language. The formal semantics of SysML/KAOS models is specified, verified, and validated using the Event-B method. Goal models provide machines and events of the Event-B specification while domain models provide its structural part (sets and constants with their properties and variables with their invariant). Our proposal is illustrated with a case study dealing with the specification of a localization component for an autonomous vehicle.",

author = "Steve Tueno and R{\'e}gine Laleau and Amel Mammar and Marc Frappier",

note = "Publisher Copyright: {\textcopyright} Springer Nature Singapore Pte Ltd. 2021.",

year = "2020",

month = jan,

day = "1",

doi = "10.1007/978-981-15-5054-6\_3",

language = "English",

isbn = "9789811550539",

pages = "39--58",

booktitle = "Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems",

publisher = "Springer Singapore",

}

Integrating Domain Modeling Within a Formal Requirements Engineering Method. / Tueno, Steve; Laleau, Régine; Mammar, Amel et al.
Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems: Communications of NII Shonan Meetings. Springer Singapore, 2020. p. 39-58.

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

TY - CHAP

T1 - Integrating Domain Modeling Within a Formal Requirements Engineering Method

AU - Tueno, Steve

AU - Laleau, Régine

AU - Mammar, Amel

AU - Frappier, Marc

PY - 2020/1/1

Y1 - 2020/1/1

N2 - One way to build safe critical systems is to formally model the requirements formulated by stakeholders and to ensure their consistency with respect to domain properties. This paper describes a metamodel for a domain modeling language built from OWL and PLIB. The language is part of the SysML/KAOS requirements engineering method which also includes a goal modeling language. The formal semantics of SysML/KAOS models is specified, verified, and validated using the Event-B method. Goal models provide machines and events of the Event-B specification while domain models provide its structural part (sets and constants with their properties and variables with their invariant). Our proposal is illustrated with a case study dealing with the specification of a localization component for an autonomous vehicle.

AB - One way to build safe critical systems is to formally model the requirements formulated by stakeholders and to ensure their consistency with respect to domain properties. This paper describes a metamodel for a domain modeling language built from OWL and PLIB. The language is part of the SysML/KAOS requirements engineering method which also includes a goal modeling language. The formal semantics of SysML/KAOS models is specified, verified, and validated using the Event-B method. Goal models provide machines and events of the Event-B specification while domain models provide its structural part (sets and constants with their properties and variables with their invariant). Our proposal is illustrated with a case study dealing with the specification of a localization component for an autonomous vehicle.

U2 - 10.1007/978-981-15-5054-6_3

DO - 10.1007/978-981-15-5054-6_3

M3 - Chapter

AN - SCOPUS:85102641625

SN - 9789811550539

SP - 39

EP - 58

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

PB - Springer Singapore

ER -

Integrating Domain Modeling Within a Formal Requirements Engineering Method

Abstract

Access to Document

Fingerprint

Cite this