Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned - Formal Methods: Foundations and Applications - page 179

KAOS identifies two types of goals: behavioral and soft goals. Behavioral goals
prescribe intended system behaviors declaratively whereas soft goals prescribe
preferences among alternative system behaviors. Behavior goals can be special-
ized into Achieve and Maintain goals. An Achieve goal specifies a property that
the system will achieve some time in the future, whereas a Maintain goal spec-
ifies a property that must hold at all times in the future. Functional goals can
be considered as Achieve goals.
A goal model is an AND/OR graph where higher-level goals can be refined into
lower-level sub-goals, and then, recursively, into low-level sub-goals that lead to
the satisfaction of requirements of the system-to-be. When a goal is AND-refined
into sub-goals, all of them must be satisfied for the parent goal to be satisfied.
It is possible to precise a specific tactic associated to the AND refinement: the
MILESTONE refinement tactic that consists in identifying milestone states that
must be sequentially satisfied for the parent goal to be satisfied. When a goal is
OR-refined, the satisfaction of one of them is sucient for the satisfaction of the
parent goal. A goal which cannot be further refined is assignable to an agent. An
agent is an active system component which plays some role in goal satisfaction. A
goal assignable to an agent is called a requisite. A requisite which is placed under
the responsibility of an agent of the system to-be is a requirement, whereas a
requisite which is placed under the responsibility of an agent in the environment
of the system is called an expectation.
2.2 Event-B Method
Event-B [2], an evolution of the classical B method [1], is a formal method for
modeling discrete systems by refinement. An Event-B model can be described
in terms of two basic constructs:
-Thecontext: it provides axiomatic properties of Event-B models. It con-
tains the static part of a model such as carrier sets, constants, axioms and
theorems. Carrier sets are similar to types but both, carrier sets and con-
stants, can be instantiated. Axioms describe properties of carrier sets and
constants. Theorems are derived properties that can be proved from the
axioms. Proof obligations associated with contexts are straightforward: the
stated theorems must be proved.
-Themachine: it contains the dynamic part such as variables, invariants,
theorems, events and variants. Variables v define the state of a machine.
Possible state changes are described by means of events. Each event is com-
posed of a guard G ( t, v ) and an action S ( t, v ), where t are local variables
the event may contain. Guards state the necessary condition under which an
event may occur, and actions describe how the state variables evolve when
the event occurs. The correctness of an Event-B model is defined by an in-
variant property under which every state in the system must satisfy. Every
event in the system must be shown to preserve this invariant. To verify this
requirement, the invariant preservation proof obligation has been defined.