=Paper=
{{Paper
|id=Vol-2019/mrt_4
|storemode=property
|title=Using Models at Run Time to Detect Incomplete and Inconsistent Requirements
|pdfUrl=https://ceur-ws.org/Vol-2019/mrt_4.pdf
|volume=Vol-2019
|authors=Byron Devries,Betty Cheng
|dblpUrl=https://dblp.org/rec/conf/models/DeVriesC17
}}
==Using Models at Run Time to Detect Incomplete and Inconsistent Requirements==
https://ceur-ws.org/Vol-2019/mrt_4.pdf
Using Models at Run Time to
Detect Incomplete and Inconsistent Requirements
Byron DeVries Betty H. C. Cheng
Department of Computer Science and Engineering Department of Computer Science and Engineering
Michigan State University Michigan State University
East Lansing, MI, 48823, USA East Lansing, MI, 48823, USA
Email: devri117@cse.msu.edu Email: chengb@cse.msu.edu
Abstract—The validity of run-time monitoring of system goals touch the ground (e.g., the vehicle is flipped over) would
and requirements depends on both the completeness of the invalidate the earlier assumption when the vehicle did not
requirements, as well as the correctness of the environmental accelerate. Formal design-time methods to decompose goals
assumptions. Often specifications are built with an idealized view
of the environment that leads to incomplete and inconsistent and requirements with guaranteed completeness exist [7],
requirements related to non-idealized behavior. Worse yet, re- though they are limited to only specific formal decomposition
quirements may be measured as satisfied at run time despite an rules. Design-time methods exist that are not limited to formal
incomplete or inconsistent decomposition of requirements due decomposition patterns [6], [8], but make assumptions about
to violated environmental assumptions. While methods exist to the environment that may be shown to be invalid at run
detect incomplete requirements at design time, environmental
assumptions may be invalidated in unexpected run-time environ- time. Problematically, run-time monitoring of incompletely
ments causing undetected incomplete decompositions. This paper decomposed requirements may indicate satisfaction when the
introduces Lykus, an approach for using models at run time to missing requirement(s) would be unsatisfied (e.g., the throttle
detect incomplete and inconsistent requirements decompositions is increased indicating satisfaction, but the vehicle does not
at run time. We illustrate our approach by applying Lykus accelerate). Currently, no methods exist to detect incomplete
to a requirements model of an adaptive cruise control system
from our industrial collaborators. Lykus is able to automatically and inconsistent requirements decompositions at run time in
detect instances of incomplete and inconsistent requirements order to ensure relevant requirement satisfaction assessment.
decompositions at run time. This paper describes Lykus, the extension of a design
time model-driven technique [6] to detect incomplete and
I. I NTRODUCTION inconsistent requirements decompositions at run time. Lykus
While run-time requirement monitors are intended to mea- adapts run-time monitors to ensure relevant assessment in
sure and report the satisfaction of the requirements in a the context of the physical environment and requirements
software system, they are only effective if the requirements model. While requirements in a hierarchical decomposition
are complete and consistent. Problematically, unexpected en- may be assessed directly or based on the satisfaction of the
vironmental scenarios that may lead to incomplete or inconsis- decomposed child requirements, neither method is sufficient to
tent requirements in cyber-physical systems (CPS) may also assess satisfaction alone in the presence of an incomplete or
allow run-time monitors to erroneously assess requirements inconsistent decomposition. However, by using a combination
satisfaction. For example, if a requirements decomposition of both assessments, it is possible to detect an incomplete or
is incomplete, then the decomposed requirement would be inconsistent decomposition and calculate the correct require-
satisfied even if the missing requirement(s) were unsatisfied. ment satisfaction. For example, given a parent requirement
This paper presents Lykus,1 an approach to automatically to accelerate a vehicle, it may appear that the requirement is
detect incomplete requirements coverage at run time. satisfied when all of the decomposed child requirements (e.g.,
Detecting incomplete requirements is still an active re- increase throttle) are satisfied. If the vehicle does not acceler-
search area [1], [2], [3], [4], [5], [6], which becomes more ate, then there is an incomplete requirement decomposition and
complicated when design-time environmental assumptions are additional requirements that are unrepresented are unsatisfied.
found to be invalid at run time. For example, a requirement Similarly, if the vehicle does accelerate but the decomposed
for a vehicle may be to accelerate. In an idealized system, requirements are not satisfied, then the parent requirement to
applying the throttle (e.g., pressing the gas pedal) would be accelerate is not being satisfied in the manner specified by
sufficient. However, the assumption that spinning the wheels the child requirements. Instead, it could be that the vehicle
faster due to an increased throttle affects vehicle speed may is rolling down a hill rather than accelerating via throttle. In
be found to be invalid. Given an environmental scenario with both cases, the intent of the acceleration requirement is not
low traction (e.g., ice) or where the vehicle’s wheels do not met, therefore the requirement is unsatisfied. Lykus identifies
incomplete and inconsistent decompositions at run time to dy-
1 Lykus is the mortal son of Ares, who sacrificed strangers to his father. namically modify requirement satisfaction monitors in order to
provide accurate assessments of the requirements unsatisfied. hierarchical requirements modeling approaches, high-level re-
Lykus also identifies violated environmental assumptions when quirements are defined by a collection of decomposed lower-
incomplete or inconsistent decompositions are identified at run level requirements that are necessary for the satisfaction of
time. the high-level requirement. Decomposition may occur over
Lykus uses utility functions [9] to analyze individual re- numerous levels, and it terminates when a set criteria is met.
quirements within the system specification. Rather than return The portions of KAOS goal modeling we employ realizes
the raw assessment values generated by the utility functions, Goal-Oriented Requirements Engineering (GORE) by defining
Lykus identifies incomplete requirements (i.e., additional re- the decomposition of parent goals as a graph. Either AND- or
quirements are necessary but not specified) and inconsistent OR-decompositions may be employed, where a parent require-
requirements (i.e., the system is not constrained in the manner ment is satisfied if all of its AND-decomposed requirements
defined by the requirements) at run time by comparing the are satisfied or if any of its OR-decomposed requirements are
utility function values for parent and child requirements. In satisfied [11]. KAOS goal model decomposition terminates
the case of incomplete requirements, the parent utility function when a decomposed goal can be satisfied by an agent. In cases
value is modified to be ‘unsatisfied,’ as there exists at least one where the agent measures the environment, the decomposed
requirement that should have been decomposed (but was not) goal is an environmental expectation. In cases where the agent
that is ‘unsatisfied.’ Similarly, in the case of an inconsistent performs an action as part of the system-to-be, the decomposed
satisfied requirement, the parent utility function value is also goal is a system requirement.
modified to be unsatisfied since the satisfaction did not take The models defined in this paper for use in the examples
place according to the constraints imposed by the decomposed apply portions of the KAOS goal modeling notation, but
requirements. Lykus explicitly uses the decompositions from we do not use the KAOS formal decomposition patterns or
within a hierarchically decomposed goal model, typically a other formal KAOS modeling methods. As Lykus is generally
design-time model, to analyze the decomposition completeness applicable to any hierarchical goal and requirement model-
and consistency at run time. ing framework, we use the terms goals and requirements
The contributions of this paper are as follows: interchangeably throughout this paper. Practically, the role of
• We introduce a run-time approach to automatically detect goals, requirements, and expectations are generally differen-
incomplete and inconsistent requirement decompositions tiated, however we treat them identically during analysis. In
in hierarchical requirements models. this paper, goal and requirement model labels are in bold
• We adapt the utility function results in the case of courier font, while variable names, goal and requirement
incomplete and inconsistent decompositions to correctly text, and emphasis are indicated by italics.
assess satisfaction in relation to the physical environment, 1) Complete Decomposition: Parent requirements are com-
as opposed to an environmental model. pletely decomposed if the satisfaction of the aggregate decom-
• We identify the environmental assumptions that are posed child requirements ensures that the parent requirement
shown to be invalid and are the contributing factor to is satisfied. That is, a requirement is incompletely decom-
the incomplete or inconsistent decomposition. posed if the decomposed requirements are satisfied yet the
• We present a prototype implementation of the Lykus run- parent requirement remains unsatisfied. In that case, at least
time analysis and requirement assessment approach. an additional requirement is necessary to satisfy the parent
• We demonstrate the applicability of Lykus on an adaptive requirement. More formally, the satisfaction of the decom-
cruise control (ACC) system implemented on a rover posed requirements (i.e., R1 , R2 , R3 , R... , Rn ), along with any
vehicle. domain properties and assumptions (i.e., Dom) ensure that
The remainder of this paper is organized into the following the parent requirement (i.e., R) is satisfied as illustrated in
sections. Section II provides an overview of background infor- Equation (1) [11].
mation. Section III details the approach. Section IV describes
an example application, and Section V details related work. {R1 , R2 , R3 , R... , Rn , Dom} R. (1)
Finally, Section VI discusses the conclusions and avenues of
future work.
2) Consistent Decomposition: Decomposed requirements
II. BACKGROUND are one method of constraining the parent requirement to a
single desirable solution, amongst potentially numerous other
This section covers background information on hierarchical possible decompositions. For example, if a parent requirement
requirements modeling, utility functions, and the Adaptive is to stop a vehicle, then two alternative solutions would
Cruise Control (ACC) system used in this paper. be to apply the brakes or remove the engine. Clearly one
solution is undesirable. Consistent decomposition implies that
A. Hierarchical Requirements Modeling the parent requirement satisfaction is only achieved when
Hierarchical requirements are applicable to multiple require- the desired solution is achieved. That is, the solution (i.e.,
ment frameworks including i* [10], KAOS goal modeling [11], decomposed requirements, R1 , R2 , R3 , R... , Rn , and domain
and hierarchical requirements modeling [12]. Intrinsic to all properties, Dom) also prevent undesired solutions of the par-
ent requirement (i.e., R). Formally this is defined in Equation C. Adaptive Cruise Control Systems
(2). Figure 2 details a hierarchical goal and requirements model
R {R1 , R2 , R3 , R... , Rn , Dom}. (2) of an Adaptive Cruise Control (ACC) system that uses distance
B. Utility Functions sensors to ensure a safe following distance from the car ahead
by adjusting vehicle speed while simultaneously maintaining
The satisfaction of requirements has been assessed by run- as close to the desired speed as possible. Abbreviations M and
time monitors [13], [14] implemented as utility functions [15]. A are used for Maintain and Achieve, respectively. Leaf nodes
While typically a Boolean expression, satisficement may be (i.e., agents) that are numbered in the requirements model
used to represent a degree of satisfaction [16], similar to the are provided in TABLE I. The ACC model defined here has
concept of satisficing [17] but without the assumption of suf- been previously shown to be complete [6], given the assumed
ficiency (i.e., the amount of satisfaction may not be sufficient environmental conditions.
for the system). The utility functions used in this paper are
generated from three sources used to capture environmental TABLE I: Agents used in Goal Model
properties (ENV, MON, REL) by Athena [9], and are defined # Agent (Sensor / Actuator)
as follows: 1 Cruise Switch Sensor
• ENV defines environmental properties related to the 2 Cruise Active Sensor
3 Cruise Active Switch
satisfaction of the goal that may or may not be directly 4 Throttle Pedal Sensor
observable (e.g., the expected speed of a vehicle at a 5 Throttle Actuator
future time), 6 Brake Pedal Sensor
7 Brake Actuator
• MON defines monitors (e.g., agents and sensors) in the
8 Speed Sensor 1
system that are able to monitor specific values (e.g., a 9 Speed Sensor 2
speed sensor that measures the speed of a vehicle at the 10 Distance Sensor 1
current time), and 11 Distance Sensor 2
• REL represents relationships between the monitors and
environmental properties that relate to the satisfaction The ACC model in Figure 2 is defined by four primary
or satisficement of goals (e.g., relating expected future components: cruise control modes (i.e., goals with a prefix
vehicle speed and current vehicle speed to measure the of ‘A.’), speed increase (i.e., goals decomposed from C.1),
satisficement of a requirement to increase speed). speed decrease (i.e., goals decomposed from B.2), and main-
The REL properties are used by Athena to compute the tain speed (i.e., goals decomposed from D.1). The speed is
degree of satisfaction (i.e., satisficement) of a requirement, increased or decreased to maximize speed up to the desired
and returns the value as either state-, metric-, or fuzzy-logic speed while maintaining a safe distance from the target car
based values. Domain properties (e.g., a throttle increase will (i.e., the car immediately in front). In cases where the safe
spin the wheels faster causing acceleration) used by Athena [9] distance is violated, the speed is decreased regardless of the
to generate utility functions are present in the environmental desired speed. In cases that both the desired speed and safe
properties (ENV, MON, and REL) specified by the system distance are met, the speed is maintained.
designer [18] based on their knowledge of the environment Goal C.1, which is used throughout as an example, is de-
and domain. composed into three children: C.2, C.3, and C.12. The Goal
For example, the utility function created for Goal C.1, C.1 (‘Achieve(Faster Speed)’) increases the speed by increas-
where the speed in the future (Speedt+1 ) must be greater ing the throttle via Goal C.3 (‘Achieve(Increase Throttle)’).
than the current speed (Speedt ) in order to achieve a faster The throttle is increased while ensuring braking is minimized
speed, results in the utility function shown in Figure 1. via Expectation C.12 when the Speed is less than the
Desired Speed (Expectation C.4) and the Distance measured
is greater than the defined Safe Distance (Expectation C.9).
bool sat_of_c1 ( ) { The utility functions for the requirements in Figure 2 are de-
/ / A s s e s s REL s a t i s f a c t i o n rived from the ENV, MON, and REL properties in TABLE II,
i f ( speed_t < speed_t_plus_1 ) { where, for brevity, only values related to the ongoing example
/ / Return s a t i s f i e d presented in this paper are presented. TABLE III defines the
return 1.0; variable value ranges and units.
} else {
/ / Return u n s a t i s f i e d III. A PPROACH
return 0.0; An overview of Lykus is presented in a Data Flow Diagram
} (DFD) in Figure 3. Processing elements are represented by
} circles. Persistent data is represented by parallel horizontal
bars. The labeled arrows indicate data flows, and boxes
Fig. 1: Utility Function Listing of C.1 represent external entities. Lykus makes use of Athena [9]
to generate the utility functions that are used as run-time
A.1 M(Adaptive Cruise System)
B.2
A(Slower Speed)
A(Off, Off) M(Off, Off) M(On, Off) M(On, On)
A.2 A.3 A.4 A.5 B.3
A(Slow Car)
B.1
A.6 A.7 A.8 A.11 A.12 A.13 A.14 M(Automatic Control) B.4
= Off = On A(Off) A.9 A.10 = On = Off = On = On
A(Reduce Throttle)
= Off = Off
1 2 3 1 2 1 2
1 2 B.5 B.6 B.7
A(Throttle Actuator = A(Throttle Pedal Throttle Angle > 0
A.15 Throttle Pedal Sensor - 1) Sensor Reading)
M(Manual Control) B.8
Speed > Desired Speed OR 4
4
Distance < Safe Distance 5
A.16 A.17
M(Throttle M(Brake Response) B.9
Speed > B.10
Response) Distance <
Desired Speed
Safe Distance
A.21 B.11 B.12
A.18 A.19 A.20 Wheel Speed > GPS Speed > B.13 B.14
A(Throttle Pedal A(Throttle Actuator = A(Brake Pedal A(Brake Actuator = Distance 1 < Distance 2 < B.15
Desired Speed Desired Speed
Sensor Reading) Throttle Pedal Sensor) Sensor Reading) Brake Pedal Sensor Safe Distance Safe Distance
A(Increase Brake)
Reading)
8 9
4 10 11
5 6
7
B.16 B.17 B.18 B.19
C.1 A(Brake Actuator = A(Brake Pedal Throttle Pedal Brake Pedal
A(Faster Speed) Brake Pedal Sensor + 1) Sensor Reading) Sensor = 0 Sensor < 45
7 6 4 6
C.2 C.3 D.1
Speed < Desired Speed AND M(Speed)
A(Increase Throttle)
Distance > Safe Distance
C.12 D.New2
C.4 A(Brake Angle = 0) A(Brake Pedal Sensor Reading)
D.3
C.5
Speed < Desired Speed A(Throttle Actuator = D.2 A(Throttle Actuator =
Throttle Pedal Speed = Desired Speed AND Throttle Pedal Sensor)
7 D.New1 6 Distance > Safe Distance
Sensor + 1)
C.6 C.7 C.8 A(Brake Actuator = 5
Brake Pedal Sensor) D.5
Wheel Speed Sensor < GPS Speed Sensor < 5 Throttle Angle < 45 D.4 A(Throttle Pedal Sensor Reading)
Desired Speed Desired Speed
C.9 Speed = Desired Speed
7 D.8
Distance > Safe Distance 4 Distance > Safe Distance 4
8 9
D.6 D.7
Wheel Speed Sensor = GPS Speed Sensor =
C.10 C.11 C.13 D.9 D.10
Desired Speed Desired Speed
Distance Sensor 1 > Distance Sensor 2 > A(Throttle Pedal Distance Sensor 1 > Distance Sensor 2 >
Safe Distance Safe Distance Sensor Reading) Safe Distance Safe Distance
8 9
10 11 4 10 11
Fig. 2: Adaptive Cruise Control Goal Model
TABLE II: ENV, MON, and REL Properties
ENV MON REL
C.1 Speedt , Speedt+1 Speedt < Speedt+1
C.2 Speedt , Distance Desired Speed, Safe Distance Speedt < Desired Speed ∧ Distance > Safe Distance
C.3 Throttle Actuator, Throttle Pedal Sensor Throttle Actuator > Throttle Pedal Sensor
C.12 Brake Actuator Brake Actuator == MIN
Speedt Speed Sensor 1, Speed Sensor 2 Speed Sensor 1 ∨ Speed Sensor 2
Speedt Throttle Pedal Sensor, Brake Pedal Sensor max(MIN, Throttle Pedal Sensor − Brake Pedal Sensor)
Speedt+1 Throttle Actuator, Brake Actuator max(MIN, Throttle Actuator − Brake Actuator)
Distance Distance Sensor 1, Distance Sensor 2 Distance Sensor 1 ∨ Distance Sensor 2
monitors to detect incomplete and inconsistent decompositions generated by Lykus is used at run time to monitor the system
of parent requirements in the goal model (e.g., Figure 2) using to detect counterexamples and accurately report satisfaction
the properties in TABLE II. Optionally, Ares can be used to throughout the system’s execution.
detect incomplete requirements decompositions that can be Lykus is applicable to systems that interact with their
identified at design-time [6]. The utility functions and goal environment, where the environment is anything that is outside
model are then used by Lykus to generate logical expressions of the system-to-be. The environment may be other systems,
that represent the decompositions within the hierarchically rather than a physical environment. Additionally, the system
decomposed goal model to detect both incomplete and in- must be able to sense its expected impact on the environment
consistent decompositions. These logical expressions are used to allow utility functions to measure the satisfaction of individ-
by Lykus to generate executable monitoring code that detects ual requirements directly, or indirectly using relationships be-
incomplete and inconsistent decompositions and accurately tween multiple sensors. Finally, requirements must be defined
report parent satisfaction. The executable monitoring code hierarchically to detect decompositional counterexamples.
TABLE III: Units and Scaling for Variables in TABLE II TABLE IV: Satisfaction Cases
Variable Min Max Unit Utility Function Updated
Speedt 0.0 100.0 MPH Parent Child Parent
Row
Speedt+1 0.0 100.0 MPH Requirement Requirements Requirement
Distance 0.0 50.0 Inches 1 Unsatisfied Unsatisfied Unsatisfied
Desired Speed 0.0 100.0 MPH 2 Unsatisfied Satisfied Unsatisfied
Safe Distance 0.0 50.0 Inches 3 Satisfied Unsatisfied Unsatisfied
Throttle Actuator 0.0 100.0 % 4 Satisfied Satisfied Satisfied
Throttle Pedal Sensor 0.0 100.0 %
Brake Actuator 0.0 100.0 % child requirement satisfaction results listed in TABLE IV are
Brake Pedal Sensor 0.0 100.0 % discussed in the following subsections. If the parent’s and
Distance Sensor 1 0.0 50.0 Inches
Distance Sensor 2 0.0 50.0 Inches decomposed child requirements’ satisfactions do not match,
Speed Sensor 1 0.0 100.0 MPH then the parent must be unsatisfied due to either incomplete or
Speed Sensor 2 0.0 100.0 MPH inconsistent decomposition. TABLE IV identifies the possible
Cruise Switch Sensor Off On Boolean
combinations of parent and decomposed child requirements
Cruise Active Sensor Off On Boolean
Cruise Active Switch Off On Boolean satisfaction, along with the updated parent satisfaction based
on run-time satisfaction measures.
1) Standard Unsatisfied Requirements: In the case where
Goals Goals & (Optional)
Goal Model Athena
Utility Functions Ares both the parent and the child requirements are unsatisfied
(i.e., Row 1 in TABLE IV), the satisfaction of the parent does
(Complete)
Run-Time Goals & not change and the parent requirement remains unsatisfied
Utility Functions
Monitoring at run time. Since both the utility function representing the
Code
Process Key: satisfaction of the parent requirement and the combined sat-
Process
Run-Time
Monitoring
Flow isfaction of child requirements are both unsatisfied, then the
External I/O
Code result is neither incomplete nor inconsistent. That is, there is
File
not a known missing requirement due to an unsatisfied parent
(2)
Generate Logical
(1) requirement nor is there an inappropriately satisfied parent
Expressions Generate Logical
Monitoring
Code
Expressions requirement due to a solution not specified by the decomposed
child requirements. When a parent requirement is unsatisfied,
we would normally expect the decomposed child requirements
Fig. 3: Lykus Data Flow Diagram
to be unsatisfied.
A. DFD Step 1: Generate Logical Expression 2) Unsatisfied Due to Incompleteness: In the case where
the parent is unsatisfied, yet the decomposed child require-
The input to Step 1 is a goal model that may be analyzed at ments are satisfied (i.e., Row 2 in TABLE IV), the parent
design-time for incomplete requirement decompositions using requirement should remain unsatisfied due to an incomplete
Ares [6] and utility functions generated by Athena [9]. Lykus decomposition. While the aggregate child requirements indi-
outputs a set of requirements monitors and additional logic cate that the parent requirement should be satisfied, they only
that detects incomplete and inconsistent requirements decom- indicate satisfaction due to a missing requirement that would
position and provides the status of the parent requirement alter the satisfaction of the aggregate set.
satisfaction. 3) Unsatisfied Due to Method Used: In the case where
Unlike design-time solutions that use utility functions for the parent requirement is satisfied, yet the decomposed child
analysis across an entire range of possible scenarios [6], Lykus requirements are unsatisfied (i.e., Row 3 in TABLE IV), the
applies the utility value functions at run time for a single parent status must be modified to indicate that it is unsatisfied.
scenario that the system is currently experiencing. Based on While the parent requirement utility function indicates that the
the results of the comparisons of the realized utility value parent requirement is satisfied, the method of satisfaction is
functions, analysis is performed each time the utility functions not constrained to the solution provided by the decomposed
are calculated at run time. Counterexamples are identified, and requirements.
subsequently adapted immediately as needed on the run-time 4) Standard Satisfied Requirement: In the case where the
requirement assessments. parent requirement and the decomposed child requirements are
TABLE IV lists the satisfaction of both the parent require- both satisfied (i.e., Row 4 in TABLE IV), then the decomposi-
ment and the set of decomposed child requirements along with tion is neither incomplete nor inconsistent. Regardless of the
the updated parent requirement satisfaction status to reflect method of assessing the requirement (i.e., directly or via the
the run-time evaluation of the parent in actual environmental requirement’s decomposed child requirements) the assessment
conditions. For each decomposed requirement, two additional results in satisfaction for both the parent and children.
checks are performed, one for incomplete decomposition and
one for inconsistent composition. If the requirement is neither B. DFD Step 2: Generate Monitoring Code
incomplete nor inconsistent, then the requirement’s utility The logic for comparing parent requirement and aggregate
function is unmodified. The possible parent and decomposed child requirements satisfactions is generated for each decom-
posed parent requirement. Neither direct measurement of each identifying an incomplete or inconsistent requirements decom-
requirement (e.g., measuring parent requirements for satisfac- positions is computationally expensive but verifying a specific
tion) nor measuring a requirement’s aggregate decomposed incomplete or inconsistent requirements decomposition can
requirements (e.g., measuring the set of child requirements for be done very quickly. Lykus leverages the latter property
satisfaction) is sufficient to assess the satisfaction of the parent and verifies the decompositional completeness and consistency
requirement in all cases. An implementation of TABLE IV with respect to only the current environmental scenario.
to calculate the updated satisfaction of requirement C.1 at Given that utility functions are widely used as run-time
run time is given in Figure 4. This approach differs from the monitors [9] (e.g., “ sat_of_ ∗()” in Fig 3), the additional cost
Ares approach, since here we detect at run time if a single Lykus incurs is used to calculate a single Boolean expression
specific environmental and system scenario related to the based on the concrete satisfaction of the utility functions (e.g.,
current state of the system includes incomplete or inconsistent calculation of “ parent_sat == child_sat ” in Fig. 3) for each
requirements decomposition. The requirements, contents of the decomposition.
Lykus calculates if each decomposition is incomplete or
bool updated_sat_of_c1 ( ) { inconsistent for the current scenario as measured by the utility
/ / Assess Parent S a t i s f a c t i o n functions and their respective monitor properties (i.e., agents
bool p a r e n t _ s a t = sat_of_c1 ( ) ; and sensors). The utility functions are updated as new sensor
/ / Assess Aggregate Child S a t i s f a c t i o n results are available (as often as 20 times a second). When
b o o l c h i l d _ s a t = s a t _ o f _ c 2 ( ) && the utility function values are updated, the decompositions that
s a t _ o f _ c 3 ( ) && s a t _ o f _ c 1 2 ( ) ; include the requirements with updated utility function values
are checked for incompleteness. That is, the decompositions of
i f ( p a r e n t _ s a t == c h i l d _ s a t ) the requirements specification are evaluated and re-evaluated
return parent_sat ; for incompleteness throughout the execution of the system the
else { generated run-time monitoring code is deployed in.
/ / Save v a r i a b l e s and r e q u i r e m e n t D. Limitations
r e c o r d _ c o u n t e r e x a m p l e ( ‘ ‘C . 1 ’ ’ ) ;
The accuracy of Lykus is only as good as the accuracy of
the ENV, MON, and REL properties used to define the utility
/ / Unsat i f incomplete / i n c o r r e c t
functions. Additionally, counterexamples may be present in a
return false ;
scenario that occurs only between sensor readings. In such
}
cases, the values calculated by the utility functions never
}
represent an incompleteness or inconsistency and, therefore,
no counterexample is detected.
Fig. 4: Updated Utility Function Listing of C.1
IV. E XAMPLES
variables, and (when included) environmental assumptions are
recorded upon the detection of an incomplete or inconsistent This section covers examples of an incomplete requirement
requirements decomposition. Similar functions that update decomposition and an inconsistent requirement decomposition.
parent requirement status, as measured from the original utility A. Experimental Setup
functions, are provided for each of the parent requirements in
the goal model in order to detect incomplete and inconsistent The updated utility functions and detection logic are ex-
decompositions and the associated variables at run time. ecuted during the operation of a small autonomous car. The
car comprises a 16 MHz ATmega328 microcontroller, and two
C. Execution Time & Deployment speed controllers driving 4 motors turning 4 wheels. Distance
For each requirements decomposition, the computational measurements are provided by an ultrasonic sensor, speed
effort of Lykus grows linearly with respect to the number of measurements are provided by a cumulative accelerometer,
decomposed requirements, assuming a constant maximum size and user input is provided by infrared remote control.
of each utility function. Instead of calculating if a requirements The small autonomous car was placed into two different
decomposition is incomplete or inconsistent in any scenario, environmental scenarios intended to elicit the detection of both
Lykus calculates if a requirement decomposition is incomplete incomplete and inconsistent decompositions.
or inconsistent in only the current scenario (e.g., the agents
periodically read from sensors to support the calculation of B. Incomplete Requirement Decomposition
the utility functions). This is similar to checking a known NP In order to demonstrate an incomplete requirement de-
problem, SAT, for a single set of true or false assignments composition for a parent requirement, the aggregate child
rather than solving which true or false assignments satisfy the requirements must be satisfied while the parent requirement
Boolean expression. itself is unsatisfied. Using goal C.1 as an example, the car
More formally, identifying incomplete or inconsistent re- must be placed in a position where the utility function is
quirements decompositions exists in NP-Complete. That is, invalid. Specifically, the speed cannot increase over some
TABLE V: Incomplete Decomposition Values TABLE VI: Environmental Assumptions: Incompleteness
Row Variable or Goal Value Row Environmental Assumption Valid
1 Brake Actuator MIN 1 Speedt = Speed Sensor 1 ∨ Speedt = Speed Sensor 2 True
2 Brake Pedal Sensor MIN Speedt = max(MIN,
2 False
3 Desired Speed MAX Throttle Pedal Sensor − Brake Pedal Sensor)
4 Distance MAX Speedt+1 = max(MIN,
3 False
5 Distance Sensor 1 MAX Throttle Actuator − Brake Actuator)
6 Distance Sensor 2 MAX Distance = Distance Sensor 1∨
4 True
7 Safe Distance 6 Inches Distance = Distance Sensor 2
8 Speed Sensor 1 MIN
9 Speed Sensor 2 MIN TABLE VII: Inconsistent Decomposition Values
10 Speedt MIN
Row Variable or Goal Value
11 Speedt+1 MIN
1 Brake Actuator MIN
12 Throttle Actuator 80% 2 Brake Pedal Sensor MIN
13 Throttle Pedal Sensor 70% 3 Desired Speed 2 MPH
14 Goal C.1 Unsatisfied 4 Distance MAX
15 Goal C.2 Satisfied 5 Distance Sensor 1 MAX
16 Goal C.3 Satisfied 6 Distance Sensor 2 MAX
17 Goal C.12 Satisfied 7 Safe Distance 6 Inches
8 Speed Sensor 1 1.2 MPH
9 Speed Sensor 2 1.2 MPH
given time despite an increase in throttle with no braking. An 10 Speedt 1.2 MPH
environmental scenario outside of the idealized environmental 11 Speedt+1 2 MPH
model (i.e., as defined in TABLE II for rows Speedt , Speedt+1 , 12 Throttle Actuator 20%
and Distance) may elicit previously undetected incomplete 13 Throttle Pedal Sensor 20%
14 Goal C.1 Satisfied
requirement decompositions. 15 Goal C.2 Unsatisfied
In this example, we physically flip the vehicle onto its back, 16 Goal C.3 Unsatisfied
allowing none of the wheels to touch the ground. Since our 17 Goal C.12 Satisfied
idealized environmental model never considered the possibility
of rolling the vehicle over, the standard method of accelerating rollovers).
does not apply. The updated utility function code generated by Lykus is able to generate code to use utility functions to
Lykus detects an incomplete decomposition from C.1 at run detect incomplete requirements decompositions at run time to
time and records the incomplete decomposition, the system ensure run-time relevant requirements assessment.
and environmental variables, and violated environmental as-
sumptions.
C. Inconsistent Requirement Decomposition
Importantly, in order to maintain the set speed, the cruise
control system attempts to accelerate by increasing the throttle In order to demonstrate an inconsistent requirements de-
(via goal C.3) while the brake is not applied (via goal C.12); composition, the speed must increase despite not increasing
there is a safe distance to any upcoming obstacle and the the throttle. We achieve this case by allowing the vehicle to
current speed is less than the desired speed (via expectation drive off a ‘cliff,’ represented by the edge of a desk. The car
C.2). Despite these decomposed child goals being satisfied, accelerates through its fall despite not increasing the throttle.
the speed (both at the current time and in the future) are 0. Just as with the incomplete requirements decomposition, the
Due to the detected incomplete decomposition, parent goal updated utility function code generated by Lykus detects an
C.1 is reported as unsatisfied based on run-time monitored inconsistent decomposition from C.1 and records the incon-
conditions. The variables recorded for the incompleteness are sistent decomposition, the system and environmental variables,
shown in TABLE V and are limited to a resolution of 10% for and violated environmental assumptions.
percentage based values and one tenth (i.e., 0.1) for all other In this case, the ACC system accelerates without increasing
values due to the truncation of sensor and actuator resolution the throttle (via goal C.3) while the brake is not applied (via
to minimize oscillation and measurement error. goal C.12). While there is a safe distance to any upcoming
Given the list of environmental assumptions defined in obstacle the current speed is not less than the desired speed
TABLE II, the values of the counterexample variables can be (via expectation C.2). Despite not satisfying these decom-
used to identify violated environmental assumptions at run posed child goals, the speed increases due to the precipitous
time. TABLE VI includes the list of environmental assumptions drop. Due to the detected inconsistent decomposition, goal
and indicates if they are valid or not. It is important to C.1 is reported as unsatisfied, as it is not satisfied in the
note that if the optional design-time completeness detection method required by the decomposed child requirements. The
was not performed by Ares, there may be no environmental variables recorded for the inconsistency are shown in TA -
assumptions documented. In this case, TABLE VI shows that BLE VII and are limited to a resolution of 10% for percentage
rows 2 and 3 both include violated environmental assumptions based values and one tenth (i.e., 0.1) for all other values due
related to the calculation of speed from only the brake and to the truncation of sensor and actuator resolution to minimize
throttle, ignoring the possibility of outside influences (e.g., oscillation and measurement error.
Given the list of environmental assumptions previously theorem proving [11] or limit possible solutions to the formally
identified in TABLE II, TABLE VIII lists the environmental defined patterns.
assumptions and indicates their run-time validity. Similar to Tools also exists that identify single [6] or multiple [8]
the incompleteness counterexample, rows 2 and 3 both include counterexamples in hierarchical requirements decompositions
violated environmental assumptions related to the calculation at design time without restrictions on decomposition patterns
of speed from only the brake and throttle, ignoring the possi- or heavyweight formal descriptions and analysis.
bility of outside influences (e.g., drastic changes in terrain). Lykus differs by acknowledging that invalid environmen-
tal assumptions made at design time may leave incomplete
TABLE VIII: Environmental Assumptions: Inconsistency decompositions intact until they occur at run time. Lykus
Row Environmental Assumption Valid detects these incomplete decompositions at run time rather
1 Speedt = Speed Sensor 1 ∨ Speedt = Speed Sensor 2 True than at design-time and provides more accurate utility function
Speedt = max(MIN, assessment in the presence of incomplete decompositions.
2 False
Throttle Pedal Sensor − Brake Pedal Sensor)
Speedt+1 = max(MIN, B. Run-Time Monitors
3 False
Throttle Actuator − Brake Actuator)
Distance = Distance Sensor 1∨ Several frameworks exist to monitor requirements at run
4 True
Distance = Distance Sensor 2 time [13], [14], [22] that are intended to support instrumen-
Lykus is able to generate code to use utility functions to tation, diagnosis, and reconfiguration operations within the
detect inconsistent requirements decompositions at run time system. The utility functions whose values we adapt in Lykus,
to ensure run-time relevant requirements assessment. as generated by Athena [9], provide the same support with the
benefit of automatic generation from a set of environmental
D. Threats to Validity properties. Lykus differs from existing run-time monitors by
Since Lykus is most realistically validated at run time, rather detecting incomplete and inconsistent requirements at run time
than using a simulation or static analysis, the validation is and adapting the results of existing run-time monitors [9] to
limited to the finite set of scenarios that occur. We have provide more accurate results.
ensured that both inconsistent and incomplete requirements VI. C ONCLUSIONS
decompositions can be identified, however additional incon- In this paper, we have presented Lykus, a run-time approach
sistent and incomplete requirements decompositions may exist for detecting incomplete and inconsistent requirements decom-
within the requirements model. The validation of the detection position and using that information to identify invalid envi-
classification, however, is done by specific cases (i.e., TA - ronmental assumptions and unsatisfied requirements. Lykus
BLE IV) within the description of the approach. Additionally,
reports the issues detected with requirements, as well as
methods that could manage sensor uncertainty (e.g., RELAXed the invalid environmental assumptions, while automatically
goals and requirements [19]) are not included in the examples updating the results of requirements monitoring.
of incomplete and inconsistent requirements. We demonstrate Lykus on an adaptive cruise control system
V. R ELATED W ORK implemented on a robotic vehicle and developed in collabora-
tion with our industrial collaborators. We show that Lykus is
This section overviews related work, including requirements able to detect incomplete and inconsistent requirements at run
completeness and run-time monitoring of requirements. Unlike time due to invalid environmental assumptions. Specifically,
proposals to use run-time specific models to support run-time we show that while existing tools identify no incomplete
analysis [20], we use goal models intended for design time requirements, incomplete decompositions may still exist due
use for run-time analysis. to incorrect assumptions that are detectable using run-time
A. Requirements Completeness monitors.
In the future, we plan to apply Lykus to additional ex-
Multiple methods have been developed to identify incom- amples, including requirements models with RELAXed re-
plete requirements decomposition. We overview these strate- quirements [19] that make use of fuzzy logic in specifying
gies and compare them to Lykus. Obstacles to requirements requirements. Additionally, we plan to investigate how Lykus
completeness have been generated using search-based tech- can be used to trigger additional mitigations at run time due to
niques [1], however the counterexamples must be manually unsatisfied requirements that would not be detected with other
reviewed for applicability. Formal methods of guaranteeing methods.
complete requirements exist for behavioral state-based sys- ACKNOWLEDGMENT
tems [21], formally described requirements using theorem This work has been supported in part by NSF grants CNS-1305358
provers [11], and low-level functional details [21]. Addi- and DBI-0939454, Air Force Research Lab grant, Ford Motor Com-
tionally, decomposition with formally-proven completeness pany, and General Motors Research. Any opinions, findings, and
properties also exist, where a system defined by repeated conclusions or recommendations expressed in this material are those
application of the formal decomposition patterns guarantees of the author(s) and do not necessarily reflect the views of the
completeness. Problematically, formal methods are intrinsi- National Science Foundation, Air Force Research Lab, Ford, GM,
cally heavyweight solutions that often require expertise with or other research sponsors.
R EFERENCES ceedings of the Third IEEE International Symposium on. IEEE, 1997,
pp. 226–235.
[1] D. Alrajeh, J. Kramer, A. v. Lamsweerde, A. Russo, and S. Uchitel,
“Generating obstacle conditions for requirements completeness,” in Pro- [11] A. Van Lamsweerde et al., “Requirements engineering: from system
ceedings of the 34th International Conference on Software Engineering. goals to uml models to software specifications,” 2009.
IEEE Press, 2012, pp. 705–715. [12] J. Souyris, V. Wiels, D. Delmas, and H. Delseny, “Formal verification
[2] B. H. C. Cheng and J. M. Atlee, “Research directions in requirements of avionics software products,” in International Symposium on Formal
engineering,” in 2007 Future of Software Engineering. IEEE Computer Methods. Springer, 2009, pp. 532–546.
Society, 2007, pp. 285–303. [13] M. S. Feather, S. Fickas, A. Van Lamsweerde, and C. Ponsard, “Recon-
[3] A. Ferrari, F. dell’Orletta, G. O. Spagnolo, and S. Gnesi, “Measuring ciling system requirements and runtime behavior,” in Proceedings of the
and improving the completeness of natural language requirements,” in 9th international workshop on Software specification and design. IEEE
Requirements Engineering: Foundation for Software Quality. Springer, Computer Society, 1998, p. 50.
2014, pp. 23–38.
[4] I. Menzel, M. Mueller, A. Gross, and J. Doerr, “An experimental [14] S. Fickas and M. S. Feather, “Requirements monitoring in dynamic
comparison regarding the completeness of functional requirements spec- environments,” in Requirements Engineering, 1995., Proceedings of the
ifications,” in Requirements Engineering Conference (RE), 2010 18th Second IEEE International Symposium on. IEEE, 1995, pp. 140–147.
IEEE International. IEEE, 2010, pp. 15–24. [15] W. E. Walsh, G. Tesauro, J. O. Kephart, and R. Das, “Utility functions
[5] M. M. Zenun and G. Loureiro, “A framework for dependability and com- in autonomic systems,” in Autonomic Computing, 2004. Proceedings.
pleteness in requirements engineering,” in Latin American Symposium International Conference on. IEEE, 2004, pp. 70–77.
on Dependable Computing, 2013, pp. 1–4. [16] J. Whittle, P. Sawyer, N. Bencomo, and B. H. C. Cheng, “A language
[6] B. DeVries and B. H. Cheng, “Automatic detection of incomplete for self-adaptive system requirements,” in Service-Oriented Computing:
requirements via symbolic analysis,” in Proceedings of the ACM/IEEE Consequences for Engineering Requirements, 2008. SOCCER’08. Inter-
19th International Conference on Model Driven Engineering Languages national Workshop on. IEEE, 2008, pp. 24–29.
and Systems. ACM, 2016, pp. 385–395.
[7] R. Darimont and A. Van Lamsweerde, “Formal refinement patterns [17] H. A. Simon, “Rational choice and the structure of the environment.”
for goal-driven requirements elaboration,” in ACM SIGSOFT Software Psychological review, vol. 63, no. 2, p. 129, 1956.
Engineering Notes, vol. 21, no. 6. ACM, 1996, pp. 179–190. [18] B. H. C. Cheng, P. Sawyer, N. Bencomo, and J. Whittle, “A goal-based
[8] B. DeVries and B. H. Cheng, “Automatic detection of incomplete modeling approach to develop requirements of an adaptive system with
requirements using symbolic analysis and evolutionary computation,” environmental uncertainty,” in Model Driven Engineering Languages
in Search Based Software Engineering - 9th International Symposium, and Systems. Springer, 2009, pp. 468–483.
SSBSE 2017, Paderborn, Germany, September 9-11, 2017, Proceedings.
[19] J. Whittle, P. Sawyer, N. Bencomo, B. H. Cheng, and J.-M. Bruel,
ACM, 2017, pp. 49–64.
“Relax: Incorporating uncertainty into the specification of self-adaptive
[9] A. J. Ramirez and B. H. C. Cheng, “Automatic derivation of utility
systems,” in Requirements Engineering Conference, 2009. RE’09. 17th
functions for monitoring software requirements,” in Model Driven
IEEE International. IEEE, 2009, pp. 79–88.
Engineering Languages and Systems. Springer, 2011, pp. 501–516.
[21] M. P. Heimdahl and N. G. Leveson, “Completeness and consistency
[10] E. S. Yu, “Towards modelling and reasoning support for early-phase
in hierarchical state-based requirements,” Software Engineering, IEEE
requirements engineering,” in Requirements Engineering, 1997., Pro-
Transactions on, vol. 22, no. 6, pp. 363–377, 1996.
[20] F. Dalpiaz, A. Borgida, J. Horkoff, and J. Mylopoulos, “Runtime
goal models: Keynote,” in Research Challenges in Information Science [22] W. N. Robinson, “Monitoring software requirements using instrumented
(RCIS), 2013 IEEE Seventh International Conference on. IEEE, 2013, code,” in System Sciences, 2002. HICSS. Proceedings of the 35th Annual
pp. 1–11. Hawaii International Conference on. IEEE, 2002, pp. 3967–3976.