Verification of Non-Functional Requirements Using Formal Semantics Danielle Gaither Department of Computer Science and Engineering University of North Texas Denton, Texas USA dcg0063@unt.edu Abstract—Studies have shown that finding defects in a software A. The Causal Component Model system is much cheaper in terms of both money and time spent when done during requirements analysis, as opposed to devel- The purpose of CCM is to analyze a given set of require- opment or testing. To this end, significant advances have been ments for the purpose of detecting potential unexpected system made in the early detection of system defects. However, research behaviors [3]. Further details about the CCM method are on exposing unexpected system behaviors is relatively scant, described in Section III. especially regarding to non-functional requirements (NFRs). We propose a model-driven approach grounded in formal semantics B. Related Work to expose unexpected behaviors in a set of NFRs and propose future work for evaluating the effectiveness of such an approach. Many approaches to the RE process are model-based in some form, such as goal-oriented and scenario-based ap- proaches. Goal-oriented approaches consider a system from I. I NTRODUCTION the perspective of the goals intended to be satisfied by that Boehm and Basili [1] claim that remedying software defects system [5]. The goals are often expressed in terms of an can be 100 times more expensive during testing than dur- ontology specific to the domain of the problem at hand ing requirements gathering. Requirements engineering (RE) [6]. A scenario-based approach considers the system as an involves eliciting natural language requirements from system aggregation of potential use-cases [7]. Both approaches can be stakeholders and trying to impose a structure on that informa- and have been used at varying levels of abstraction to construct tion [2]. Most approaches to the RE process rely on using the system models. However, Carrillo de Gea et al. [8] note that requirements to derive one or more models of some aspect of requirements modeling is one of the least supported features the system, such as data or behavior. among current RE tools. Combining a model-based approach One such requirements analysis solution is the Causal with the detection of unexpected behaviors and the addition Component Model (CCM) [3], which attempts to expose un- of NFRs can therefore contributing to advancing the state of expected behaviors in a system. Although Foyle and Hooey [4] RE as a whole. raised concerns about the lack of accounting for unexpected Bryant et al. [9] discussed some of the benefits and chal- behaviors in RE tools in 2003, very little work has been done lenges of formalizing the semantics of domain-specific model- in this area since then. We believe that a requirements analysis ing languages. One benefit is amenability to formal verification tool in this domain should be able to analyze non-functional methods, which is well-suited to safety- and security-critical requirements such as timing and security properties. Many re- systems. Hessel et al. [10] used timed automata via the quirements analysis methods either focus solely on functional UPPAAL model checker [11] to generate test cases for a real- requirements, or on later stages of system implementation [3]. time system. Lee and Bryant [12] implemented a two-level The remainder of this paper will be structured as follows: grammar using VDM++, the Vienna Development Method first will be discussions of CCM and a survey of related work meta-language [13]. in the area, including an explanation of how our proposed work improves upon existing approaches. The next section III. A PPROACHES AND G OALS includes a discussion of the approaches and goals intended This section will outline the goals of the intended work for the proposed work, including the research questions to be and the approaches to be studied. The goals of our work answered. An overview of preliminary and remaining work are: creating a formal semantics for quantifiable NFRs, and will follow, as well as a discussion of the merit and impact of applying the created semantics to a requirements analysis tool. the proposed work. The paper will end with a brief conclusion. Our approach is explained in Figure 1. II. BACKGROUND AND R ELATED W ORK A. Establishing a Formal Semantics for Quantifiable NFRs In this section we provide background on the causal com- The approach for creating the formal semantics will be ponent model (CCM), first proposed by Aceituna and Do [3], based on a timed denotational semantics, and the requirements and provide a survey of related work in the field. analysis process will use the CCM tool as an example. These Fig. 1: An overview of the proposed approach. are represented by the external inputs in the diagram in Figure are satisfied with the quality of the CCM instance (Step 4 in 1. Figure 1). The process begins with requirements elicitation (Step 1 There is some precedent in the literature for creating and in Figure 1). The elicited requirements will then be used to using a formal semantics for timed operations. Li [14] used create a CCM instance (Step 2 in Figure 1). This information duration calculus to extend the RAISE specification language will serve as an input to create specific semantics for that to support timed operations. Duration calculus is an extension CCM instance based on the larger semantic specification (Step of interval logic [15]. 3 in Figure 1). Step 3a is optional, involving Coq’s code generation capabilities, which can be combined with other B. Applying Formal Semantics to the Requirements Analysis code for analysis purposes. Process The analysis will attempt to detect unexpected behaviors in Since the idea of the CCM approach is to find system defects NFRs for real-time embedded systems. If unexpected behav- in the requirements-analysis phase, the lack of an actual iors are found, the process returns to the elicitation phase for system presents particular difficulties with regard to NFRs. clarification. The whole process is repeated until all parties An alternative approach is to verify such properties logically by creating a formal semantic specification and analyzing said A denotational semantics was created for the MicroRPG specification with currently existing tools. metamodel and implemented in Haskell [20]. Current work The proposed changes to the CCM involve expanding the is focused on establishing a denotational semantics based on rule application and analysis phases. A formal semantics will statecharts that can then be applied to analysis frameworks be created for quantifiable NFRs, and the semantics will be such as CCM. used to check the validity of the NFRs. Note that the basic CCM approach does not change. The proposed updates merely B. Summary of Preliminary and Remaining Work broaden its scope. While the change might appear cosmetic, the implementation will require structural change in the CCM Our preliminary work in this area has shown the potential tool, as representing timed operations adds some complexity benefits of providing a formal denotational semantics for a to the implementation [16], [17], [18]. domain-specific model. We have taken the following steps: created a modeling language for a sample domain, created C. Research Questions and implemented a denotational semantics for a modeling The intent is to establish a formal denotational semantics language, and analyzed appropriate domains for a formal for CCM for the purpose of supporting non-functional re- semantics-based requirements analysis tool. quirements, including timing information. The research should We have recently completed a pilot study that uses state- answer the following questions: charts as the basis for a formal semantics. The results of this RQ1. How can we add formal semantics to a requirements pilot study have been accepted for publication [21]. analysis system, such as CCM, to incorporate NFRs? The following work remains to be done: establish a larger- RQ2. How does adding formal semantics and timed oper- scale denotational semantics for NFRs for real-time em- ations increase the expressiveness of a requirements bedded systems, implement the denotational semantics in analysis system? a manner consistent with a CCM implementation, use the RQ3. What properties can be proven about NFRs once a newly-enhanced CCM to verify timing properties and other formal semantics is established? quantifiable NFRs for a sample real-time embedded system, and perform empirical studies to evaluate the effectiveness of D. Evaluation Methods and Metrics proposed CCM improvements. For a tool or approach to be useful, it generally has to satisfy two main criteria. First, it needs to perform the tasks it claims to perform, and second, it needs to do so in a way that offers V. M ERIT AND I MPACT some sort of advantage over competing methods. To satisfy the Since many real-world operations are time-sensitive in some first criterion, we intend to implement the formal semantics we fashion, a robust requirements analysis system needs to be create in a theorem-proving tool such as Coq [19]. This will able to support such operations. Adding support for timed allow the correctness and completeness of the semantics to operations to CCM will make it more expressive and allow be established. To satisfy the second criterion, we expect the it to be used for more applications than is currently possible. main advantage our approach will offer will be time savings Since functional requirements and nonfunctional requirements compared to similar analysis methods. A human study will cannot be completely separated, it makes sense for a compre- be necessary to evaluate the truth of this claim. One possible hensive requirements analysis solution to handle both. Another experiment could involve groups being given the same set of benefit is that formal analysis tools can be especially useful requirements and constructing analysis models using various for mission-critical applications. Finally, a particular benefit methods. It is important to have a large enough sample size of the denotational semantics-based approach is independence to control for variations in individual ability. from a particular implementation. IV. C OMPLETED AND R EMAINING W ORK This section will describe preliminary work that has already VI. C ONCLUSIONS AND F UTURE W ORK been performed, to include: formalizing the semantics of a domain-specific modeling language, establishing the link We proposed a model-based approach for detecting unex- between domain-specific modeling and requirements analysis, pected behaviors of requirements, particularly non-functional and domain analysis with respect to requirements engineering. requirements, which have not received the same attention in research as functional requirements have to date. A. Establishing a Formal Semantics for a Domain-Specific This work is in its early stages, so there is significant poten- Modeling Language tial for future work. While timing and security requirements Preliminary work has been done in the area of creating are important, there are also things like safety requirements and implementing semantics for a domain-specific modeling to be considered. Also, we would like to build on our current language. As a proof-of-concept, the MicroRPG modeling work to analyze more complex sets of non-functional require- language was created to model a simple game. The abstract ments. Integration with existing requirements analysis tools is syntax of MicroRPG was established using a metamodel. also another priority for future work. R EFERENCES in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4949 LNCS, [1] B. Boehm and V. R. Basili, “Software defect reduction top 10 list,” 2008, pp. 77–117. Computer, vol. 34, no. 1, pp. 135–137, 2001. [11] G. Behrmann, A. David, and K. Larsen, A Tutorial on Uppaal. Springer- [2] R. Dömges, S. Jacobs, M. Jarke, H. W. Nissen, K. Pohl, N. Maiden, Verlag Berlin Heidelberg, 2004, vol. 3185. A. Sutcliffe, C. Taylor, D. Till, P. Constantopoulos, G. Spanoudakis, Y. Vassiliou, G. Grosz, V. Plihon, C. Rolland, J. R. Schmitt, S. Schwer, [12] B.-s. Lee and B. R. Bryant, “Automated conversion from requirements S. Si-Said, C. Souveyet, J. Bubenko, R. Gustas, P. Holm, P. Johannesson, documentation to an object-oriented formal specification language”,” J. Ljungberg, and B. Wangler, “Defining visions in context: Models, Proceedings of the 2002 ACM symposium on Applied computing, pp. processes and tools for requirements engineering,” Information Systems, 932–936, 2002. vol. 21, no. 6, pp. 515–547, 1996. [13] E. Dürr and J. van Katwijk, “VDM++, a formal specification language [3] D. Aceituna and H. Do, “Exposing the Susceptibility of Off-Nominal for object-oriented designs,” in Computer Systems and Software Engi- Behaviors in Reactive System Requirements,” in Proceedings of the neering. The Hague, Netherlands: IEEE, 1992, pp. 214 –219. IEEE International Requirements Engineering Conference, vol. 23. [14] L. Li, “Towards a denotational semantics of timed RSL using Duration IEEE, 2015, pp. 136–145. Calculus,” Journal of Computer Science and Technology, vol. 16, no. 1, [4] D. Foyle and B. Hooey, “Improving Evaluation and System Design pp. 64–76, 2001. Through the Use of Off-Nominal Testing: A Methodology for Scenario [15] M. R. Hansen and Z. Chaochen, “Duration Calculus : Logical Foun- Development,” in of the Twelfth International Symposium on Aviation dations,” Formal Aspects of Computing - Springer, vol. 9, no. 3, pp. Psychology, 2003. 283–330, 1997. [5] A. van Lamsweerde, “Goal-oriented requirements engineering: a guided [16] R. Alur and D. L. Dill, “A theory of timed automata,” Theoretical tour,” Proceedings Fifth IEEE International Symposium on Requirements Computer Science, vol. 126, no. 2, pp. 183–235, 1994. Engineering, pp. 249–262, 2001. [17] J. Bengtsson and W. Yi, “Timed automata: Semantics, algorithms and [6] E. Yu and J. Mylopoulos, “Why Goal-Oriented Requirements Engineer- tools,” Lecture Notes in Computer Science, vol. 3098, no. 316, pp. 87– ing,” in Proceedings of the 4th International Workshop on Requirements 124, 2004. Engineering, 1998, pp. 15–22. [7] A. G. Sutcliffe, “Supporting scenario-based requirements engineering,” [18] Ø. Haugen, K. E. Husa, R. K. Runde, and K. Stølen, “Why timed IEEE Transactions on Software Engineering, vol. 24, no. 12, pp. 1072– sequence diagrams require three-event semantics,” in International 1088, 1998. Workshop on Scenarios: Models, Transformations and Tools, vol. 3466, [8] J. M. Carrillo De Gea, J. Nicolás, J. L. Fernández Alemán, A. Toval, 2005, pp. 1–25. C. Ebert, and A. Vizcaı́no, “Requirements engineering tools: Capabil- [19] INRIA, “The Coq proof assistant,” 2016. [Online]. Available: ities, survey and assessment,” Information and Software Technology, https://coq.inria.fr vol. 54, no. 10, pp. 1142–1157, 2012. [20] D. Gaither and B. R. Bryant, “Toward Denotational Semantics of [9] B. R. Bryant, J. Gray, M. Mernik, P. J. Clarke, R. B. France, and Domain-Specific Modeling Languages for Automated Code Generation,” G. Karsai, “Challenges and directions in formalizing the semantics in Presented at the International Workshop on the Globalization of of modeling languages,” Computer Science and Information Systems, Modeling Languages, Miami, 2013. vol. 8, no. 2, pp. 225–253, 2011. [21] D. Gaither, H. Do, and B. R. Bryant, “Toward detection of abnormal [10] A. Hessel, K. G. Larsen, M. Mikucionis, B. Nielsen, P. Pettersson, and behaviors in timing and security requirements,” in 24th Asia-Pacific A. Skou, “Testing real-time systems using UPPAAL,” in Lecture Notes Software Engineering Conference (to be published), 2017.