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.