The SysML/KAOS Domain Modeling Approach

TL;DR

This paper presents a formal domain modeling approach integrating SysML/KAOS with OWL, PLIB, and Event-B to ensure consistency and correctness in critical system requirements, demonstrated through an autonomous vehicle localization case study.

Contribution

It introduces a formal metamodel for SysML/KAOS domain modeling using OWL and PLIB, with semantics represented in Event-B, enhancing requirement consistency and system correctness.

Findings

Successful modeling of a localization component for an autonomous vehicle

Formal semantics enable verification of system requirements

Case study demonstrates practical applicability of the approach

Abstract

A means of building safe critical systems consists of formally modeling the requirements formulated by stakeholders and ensuring their consistency with respect to application domain properties. This paper proposes a metamodel for an ontology modeling formalism based on OWL and PLIB. This modeling formalism is part of a method for modeling the domain of systems whose requirements are captured through SysML/KAOS. The formal semantics of SysML/KAOS goals are represented using Event-B specifications. Goals provide the set of events, while domain models will provide the structure of the system state of the Event-B specification. Our proposal is illustrated through a case study dealing with a Cycab localization component specification. The case study deals with the specification of a localization software component that uses GPS,Wi-Fi and sensor technologies for the realtime localization of the Cycab vehicle, an autonomous ground transportation system designed to be robust and completely independent.