-Studies have shown that finding defects in a software system is much cheaper in terms of both money and time spent when done during requirements analysis, as opposed to development or testing. To this end, significant advances have been made in the early detection of system defects. However, research on exposing unexpected system behaviors is relatively scant, especially regarding to non-functional requirements (NFRs). We propose a model-driven approach grounded in formal semantics to expose unexpected behaviors in a set of NFRs and propose future work for evaluating the effectiveness of such an approach.
Boehm and Basili [
One such requirements analysis solution is the Causal
Component Model (CCM) [
The remainder of this paper will be structured as follows: first will be discussions of CCM and a survey of related work in the area, including an explanation of how our proposed work improves upon existing approaches. The next section includes a discussion of the approaches and goals intended for the proposed work, including the research questions to be answered. An overview of preliminary and remaining work will follow, as well as a discussion of the merit and impact of the proposed work. The paper will end with a brief conclusion.
The purpose of CCM is to analyze a given set of
requirements for the purpose of detecting potential unexpected system
behaviors [
Many approaches to the RE process are model-based in
some form, such as goal-oriented and scenario-based
approaches. Goal-oriented approaches consider a system from
the perspective of the goals intended to be satisfied by that
system [
Bryant et al. [
This section will outline the goals of the intended work and the approaches to be studied. The goals of our work are: creating a formal semantics for quantifiable NFRs, and applying the created semantics to a requirements analysis tool. Our approach is explained in Figure 1.
In this section we provide background on the causal
component model (CCM), first proposed by Aceituna and Do [
The approach for creating the formal semantics will be based on a timed denotational semantics, and the requirements analysis process will use the CCM tool as an example. These are represented by the external inputs in the diagram in Figure 1.
The process begins with requirements elicitation (Step 1 in Figure 1). The elicited requirements will then be used to create a CCM instance (Step 2 in Figure 1). This information will serve as an input to create specific semantics for that CCM instance based on the larger semantic specification (Step 3 in Figure 1). Step 3a is optional, involving Coq’s code generation capabilities, which can be combined with other code for analysis purposes.
The analysis will attempt to detect unexpected behaviors in NFRs for real-time embedded systems. If unexpected behaviors are found, the process returns to the elicitation phase for clarification. The whole process is repeated until all parties are satisfied with the quality of the CCM instance (Step 4 in Figure 1).
There is some precedent in the literature for creating and
using a formal semantics for timed operations. Li [
Since the idea of the CCM approach is to find system defects in the requirements-analysis phase, the lack of an actual system presents particular difficulties with regard to NFRs. An alternative approach is to verify such properties logically by creating a formal semantic specification and analyzing said specification with currently existing tools.
The proposed changes to the CCM involve expanding the
rule application and analysis phases. A formal semantics will
be created for quantifiable NFRs, and the semantics will be
used to check the validity of the NFRs. Note that the basic
CCM approach does not change. The proposed updates merely
broaden its scope. While the change might appear cosmetic,
the implementation will require structural change in the CCM
tool, as representing timed operations adds some complexity
to the implementation [
The intent is to establish a formal denotational semantics for CCM for the purpose of supporting non-functional requirements, including timing information. The research should answer the following questions:
RQ1. How can we add formal semantics to a requirements analysis system, such as CCM, to incorporate NFRs? RQ2. How does adding formal semantics and timed operations increase the expressiveness of a requirements analysis system? RQ3. What properties can be proven about NFRs once a formal semantics is established? D. Evaluation Methods and Metrics
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
some sort of advantage over competing methods. To satisfy the
first criterion, we intend to implement the formal semantics we
create in a theorem-proving tool such as Coq [
This section will describe preliminary work that has already been performed, to include: formalizing the semantics of a domain-specific modeling language, establishing the link between domain-specific modeling and requirements analysis, and domain analysis with respect to requirements engineering.
Preliminary work has been done in the area of creating
and implementing semantics for a domain-specific modeling
language. As a proof-of-concept, the MicroRPG modeling
language was created to model a simple game. The abstract
syntax of MicroRPG was established using a metamodel.
A denotational semantics was created for the MicroRPG
metamodel and implemented in Haskell [
Our preliminary work in this area has shown the potential benefits of providing a formal denotational semantics for a domain-specific model. We have taken the following steps: created a modeling language for a sample domain, created and implemented a denotational semantics for a modeling language, and analyzed appropriate domains for a formal semantics-based requirements analysis tool.
We have recently completed a pilot study that uses
statecharts as the basis for a formal semantics. The results of this
pilot study have been accepted for publication [
The following work remains to be done: establish a largerscale denotational semantics for NFRs for real-time embedded systems, implement the denotational semantics in a manner consistent with a CCM implementation, use the newly-enhanced CCM to verify timing properties and other quantifiable NFRs for a sample real-time embedded system, and perform empirical studies to evaluate the effectiveness of proposed CCM improvements.
Since many real-world operations are time-sensitive in some fashion, a robust requirements analysis system needs to be able to support such operations. Adding support for timed operations to CCM will make it more expressive and allow it to be used for more applications than is currently possible. Since functional requirements and nonfunctional requirements cannot be completely separated, it makes sense for a comprehensive requirements analysis solution to handle both. Another benefit is that formal analysis tools can be especially useful for mission-critical applications. Finally, a particular benefit of the denotational semantics-based approach is independence from a particular implementation.
We proposed a model-based approach for detecting unexpected behaviors of requirements, particularly non-functional requirements, which have not received the same attention in research as functional requirements have to date.
This work is in its early stages, so there is significant potential for future work. While timing and security requirements are important, there are also things like safety requirements to be considered. Also, we would like to build on our current work to analyze more complex sets of non-functional requirements. Integration with existing requirements analysis tools is also another priority for future work.