# Formal Specification Based Automatic Test Generation for Embedded Network Systems

Authors: Eun Hye Choi; Hideaki Nishihara; Takahiro Ando; Nguyen Van Tang; Masahiro Aoki; Keiichi Yoshisaka; Osamu Mizuno; Hitoshi Ohsaki
Journal: Journal of Applied Mathematics
 (2014)

---

## Abstract

Embedded systems have become increasingly connected and communicate with each other, forming large-scaled and complicated network systems. To make their design and testing more reliable and robust, this paper proposes a formal specification language calledSENS and a SENS-based automatic test generation tool called TGSENS. Our approach is summarized as follows: (1) A user describes requirements of target embedded network systems by logical property-based constraints using SENS. (2) Given SENS specifications, test cases are automatically generated using a SAT-based solver. Filtering mechanisms to select efficient test cases are also available in our tool. (3) In addition, given a testing goal by the user, test sequences are automatically extracted from exhaustive test cases. We’ve implemented our approach and conducted several experiments on practical case studies. Through the experiments, we confirmed the efficiency of our approach in design and test generation of real embedded air-conditioning network systems.


---

## Body

## 1. Introduction

An embedded network system (ENS) is a system consisting of a number of embedded units that communicate with each other. Nowadays, ENSs are growing rapidly and playing an important role in our daily life, such as in-vehicle networking systems, home appliance networks, and building energy management systems. On the other hand, because of the increasing complexity of functionality and growing network scales, as well as the increasing numbers and types of embedded units in ENSs, development of the ENSs has been becoming more and more difficult. Particularly, design and test generation are ones of the most important and cost-consuming phases in reliable ENS development, but many companies still rely on the traditional techniques where system requirements are described in a natural language and test cases are generated based on human experience. However, design and test by manpower may not sufficiently cover enormous numbers of combination to be considered especially for complicated ENSs.During the last decade, numerous formal methods have been proposed to improve software quality. Especially, test generation is an attractive application for mechanized formal methods; the importance of good test cases is universally recognized and so is the high cost of generating them by hand. One of these methods, the model-based test generation, has been extensively studied (e.g., see [1–4]). One of the advantages of this technique is that each behavior of the system model is described directly, and then test cases can be automatically generated from the models. Note, however, that if test cases are generated from incomplete specifications and models, they suffer from the problem of lacking and low quality of test cases. Therefore, formal specification based modeling and test generation for large-scale ENSs are still challenges.This paper presents our works gained in a joint project ofA
I
S
T, D
a
i
K
i
n
I
n
d
u
s
t
r
i
e
s, and K
y
o
t
o
I
n
s
t
i
t
u
e
o
f
T
e
c
h
n
o
I
o
g
y. The ultimate goal of our project is to develop a robust and reliable automatic test generation tool suitable for a development process of air-conditioning network systems developed by D
a
i
k
i
n. (We refer to the company as Company D in the rest of this paper.) The target system consists of a number of embedded controllers and indoor/outdoor air-conditioning equipment for building management. For this project, we have taken an approach of automatic test generation based on a formal specification. In the following, we present three main contributions toward our overall goal.(i)
Development of a Formal Specification Language. First, we have developed a specification language for ENSs called S
E
N
S (Specification language for Embedded Network Systems). S
E
N
S is designed under the concept of test-oriented, object-oriented, modular, and lightweight description of ENSs. In S
E
N
S system, the requirements are specified using logical constraints. This logical property rigorously determines a set of state transitions that satisfy all constraints and thus helps to get the specification without lacking and inconsistency and clearly obtain an advantage over a manpower design of system and test.
(ii)
Development of a Test Case Generator. Second, we have developed a tool called T
G
S
E
N
S (Test Generator based on SENS) which automatically generates high quality test cases from a given specification written in SENS. Our tool can find distinct and enormous test cases quickly that satisfy complex specifications using a SAT solver as a core engine. Our tool can also perform filtering to select efficient test cases. In a feasibility study using air-conditioning systems of CompanyD, given a specification for a certain function of the system, our tool took only about 12 seconds to generate 77,700 test cases. We expect that our tool will provide both quality improvement and cost saving for testing target ENSs.
(iii)
Development of a Test Sequence Generator. Third, we have also developed a tool in TGSENS to generate test sequences that satisfy a given testing goal by a user. In an experiment using components of the target air-conditioning systems, our tool generated 156 test sequences in 8 minutes for a given testing goal such that the sequence contains 2 milestone states whose distance is less than 3 state transitions. We confirmed that our tool is helpful for test engineers to design test scenarios efficiently.The rest of this paper is organized as follows. In the next section, we briefly introduce the overview of our work and our tool. Section3 describes the features, syntax, and semantics of theSENS language. In Section 4, we propose the method for generating test cases and sequences fromSENS specifications. Section 5 presents experimental results when applying our tool to the air-conditioning systems of CompanyD. Section 6 discusses related works. Finally, we conclude our work and mention future works in Section 7.


## 2. Overview of Our Work

Our target system is an embedded network system (ENS). An ENS can be considered as a concurrent system consisting of multiple subsystems with global environments, for example, embedded indoor and outdoor equipment and controllers in an air-conditioning network system as illustrated in Figure1. Each subsystem in an ENS is an event-triggered system whose events are communications with other subsystems and whose operations are constrained by conditions related to its environment and time.Figure 1
An air-conditioning system and itsSENS  specification.The behaviors of an ENS are specified in a hierarchical way: an ENS consists of subsystems, a subsystem is constructed from its functions, and each function is constructed from a set of functional requirements, as described in Figure1. To enhance the reliability and efficiency of design and testing ENSs, we first focus on designing and modeling a formal specification language for ENSs, called S
E
N
S, which supports the hierarchy of ENSs and is convenient for our test generation purpose. We next achieve an automatic test generation approach based on S
E
N
S, called T
G
S
E
N
S. Figure 2 illustrates the overview of our tool that consists of the following 5 steps.(1)
Specifying Requirements in SENS. A user describes system requirements of the target ENS using S
E
N
S. For the air-conditioning systems of Company D, we have translated original specification documents written in a natural language to formal specifications in S
E
N
S.
(2)
Translating SENS Specifications to CNF. The S
E
N
S translator first performs the syntax and type checking for the given S
E
N
S specification. Next, the translator automatically transforms logical requirements of the S
E
N
S specification to CNF (conjunctive normal form) formulas according to our translation rules.
(3)
Solving CNF Formulas Using a SAT Solver. The CNF formulas obtained in Step (
2
) are imported as an input of the solver. The solver automatically finds all possible assignments that satisfy the input CNF formulas by iteratively using a SAT solver.
(4)
Mapping from Assignments to Test Cases. The set of possible assignments obtained in Step (
3
) are automatically mapped to the set of state transitions corresponding to one-step test cases.
(5)
Generating Test Sequences under a Testing Goal. When a user gives a testing goal including remarkable states and lengths of sequences, a set of test sequences are automatically derived from the test cases (state transitions) obtained in Step (
4
).Figure 2
An overview ofT
G
S
E
N
S.


## 3. SENS Specification

In this section, we present a compact formal language calledS
E
N
S to specify requirements of embedded network systems (ENSs). In Section 3.1, we present features of S
E
N
S. In Sections 3.2 and 3.3, we briefly describe the syntax and semantics of S
E
N
S.


### 3.1. Features of SENS

TheS
E
N
S specification is basically a set of requirements represented by logical formulas. S
E
N
S is based on a quantifier-free predicate modal logic with a next operator where predicate variables are classified into environments, systems, communication channels, and timer variables. S
E
N
S has the following features.


#### 3.1.1. Property-Based

Property-based logical formulas represent requirements which constrain system behaviors. Since a part of the specification less affects the entire specification, it is easy to modify and reuseS
E
N
S specifications. A requirement is described in a traditional Hoare triple-like way:
(1)
〈
p
r
e
:
e
v
e
n
t
:
(
p
o
s
t
,
a
c
t
i
o
n
)
〉
,
where p
r
e (resp., p
o
s
t) denotes a logical constraint holding in a prestate (resp., poststate) and an e
v
e
n
t (resp., a
c
t
i
o
n) represents a message receiving (resp., sending) between subsystems. This 3-tuple requirement needs to hold for all transitions of the system model, and we call this 3-tuple requirement a transition requirement.


#### 3.1.2. Test-Oriented

For a testing purpose, specifying tested values and bounds of variables is available in the variable declaration. This supports a test-oriented design and an efficient test generation fromS
E
N
S specifications.


#### 3.1.3. Object-Oriented

A group of subsystems is represented as a parameterized class, and each subsystem is defined as an instance of the class in the main class representing the whole system. This representation leads to an efficient description of a large number of subsystems in an ENS.


#### 3.1.4. Modular

Specifications of an ENS, a subsystem, and a function are broken down into specifications of subsystems, functions, and transition requirements, respectively. This modular construction makes it easy to specify a large-scaled and complicated ENS piece by piece and provide a reusability of specifications. This also allows a step-wise test generation fromS
E
N
S specifications for unit testing, integration testing, and system testing.


#### 3.1.5. Lightweight Description of Time Constraints

We consider a timer as a component of a subsystem and then specify time constraints using events and actions with the timer.S
E
N
S provides a timer variable which is declared with a time-value, a time-unit, and a condition formula for counting up the timer.


### 3.2.  Syntax of SENS

Here, we give the brief explanation ofS
E
N
S description using the following example embedded system.Example 1.
Consider an illustrating system in Figure3. There are 2 kinds of equipment, namely, classes A and B. Let us consider a simple ENS consisting of 3 subsystems A
1, B
1, and B
2, where A
1 is an instance of A and B
1 and B
2 are instances of B. A subsystem of class A sends a message m after 2 minutes from starting its operation. Each subsystem of class B turns on its lamp when receiving message m. This system can be described in the S
E
N
S specification of Pseudocode 1.Pseudocode 1:An example SENS specification.
<
main.cls>
(1)
Import  A,
B;
(2)
Class
main
(3)
Data
(4)
onoff_status  {on,off};
(5)
Var
(6)
B1,  B2 : B;
(7)
A1 : A(B1,  B2);
<A.cls>
(1)
Import B;
(2)
Extern
(3)
Data
(4)
onoff_status;  //from  main
(5)
Class  A(arg
1
: B,  arg2 : B)
(6)
Var
(7)
op
:
onoff_status{off};
(8)
Timer
(9)
t 2
min;
(10)
(11)
Function SendingM
(12)
Require
(13)
~
op==off && op==on
:
null
:
t!start;
(14)
op==on
:
t?ring
:
arg1.ch!m,
arg2.ch!m;
<B.cls>
(1)
Extern
(2)
Data
(3)
onoff_status; //from main
(4)
Class B
(5)
Data
(6)
m_type{m};
(7)
Var
(8)
op
:
onoff_status{off};
(9)
lamp
:
onoff_status{off};
(10)
Channel
(11)
ch
:
m_type;
(12)
(13)
Function Lighting
(14)
Require
(15)
op==on && lamp==off
:
ch?m
:
lamp==on;
(16)
op==off
−
> lamp==off;Figure 3
An example embedded system.TheS
E
N
S declarations consist of the following declarations (refer to Appendix A for the full syntax of SENS).(i) Main Class Declaration. File <main.cls>  specifies the main class. The main class represents the whole system consisting of subsystems and the environment. In the file <main.cls>  of Pseudocode 1, the classes A and B are imported in line 1, and subsystems A
1, B
1, and B
2 are instantiated in lines 6-7. Environment variables are declared in the Var part. Data types, environment variables, and channels declared in the main class are referred in all class declarations. Invariants (logical expressions) for the entire system are declared in the main class. In the example <main.cls>, global data type onoff_status  is declared in lines 3-4.(ii) Class Declaration. Files <A.cls>  and <B.cls>  of Pseudocode 1 specify classes A and B, respectively. A class other than the main class specifies a class of subsystems. Local data types, variables, channels, and timers for the subsystem are declared in the class declaration. In <A.cls>, local variable op and timer t are declared in lines 6–9, and a function of the subsystem is declared in lines 11–14.For data types, variables, channels, and timers externally declared and internally used, the files to declare them are imported with theImport statement and their names are described in the Extern part. The main class file is imported to all class files by default. A class can have parameters used as constants in the class specification. In line 1 of <A.cls>, class B is imported since class B is used in the parameter declaration of A. In lines 3-4, data type onoff_status is described in the Extern part.(iii) Variable and Data Type Declarations. A variable is declared with its name, type, initial value, and test declaration (values and bounds for testing) in the part following to Var. Data types are int and double with ranges, and enumerated data types are defined in the Data part. In the Data part, a type is defined as a set of values. In S
E
N
S, only finite and discrete values are used. In the example<main.cls>, a global data type, onoff_status, which has two elements on  and off, is declared in lines 3-4. In <B.cls>, a local data type, m_type, which has the only element m, is declared in lines 5-6. Using the test declaration beginning with the keywordtestedwith, one can define the specific values of variables to be considered in a testing phase. For example, consider the following variable declaration:Var v1 double  [
-2, 5
]  {0}
testedwith  {-2, 0..5   (0.5)};variablev1 is defined as follows: its type is double, its range is −2 ≤ v1 ≤ 5, its initial value 0, and its tested values are −2 and a number from 0 to 5 in increments of 0.5. In our semantics of S
E
N
S, each variable of a subsystem takes one value, that is, an element of its domain. If the declaration of a variable has a test declaration, the domain is defined by the test declaration. Otherwise, the domain is defined by the data type of the variable.(iv) Channel and Timer Declarations. Channels are used to describe communications between subsystems. A channel is declared with its name and message type. In lines 10-11 of <B.cls>, a channel ch for receiving message m is declared. A timer is declared with its name, time-value, unit, and conditions (logical formula) for counting up. When the condition is omitted, the condition is always true. For example, consider the following timer declarations:Timer
t1 5 min;
t2 5 hour [(v==dry) ∣∣ (v==cool)];Timert1 is declared to count up 5 minutes. Timer t2 is declared to count up 5 hours, but the counting is performed only when the value of v is dry or cool.The event is a message receiving (channel-name?expr) or timeout (timer-name?ring). Similarly, the action is a message sending (channel-name!expr), timer starting (timer-name!start), or timer reset (timer-name!clear). When specifying a communication between subsystems, a message sending (action) is described using both a recipient's object name and a channel name, while a message receiving (event) is described using only a channel name.(v) Function and Requirement Declarations. Functions are declared in the class declaration or in individual function declaration files. In the function declaration, constants, data types, variables, and timers can be defined locally. A function contains a set of requirements.A requirement is an expression representing an invariant or a 3-tuple of a precondition, an event, and a postcondition or/with/without actions. (More precisely, the third part of the transition requirement is a postcondition or an action or actions or a postcondition with an action or a postcondition with actions.) We call the 3-tuple requirement a transition requirement. The BNF description for a transition requirement is given in Algorithm1 (Refer to Appendix A.4).Algorithm 1:The BNF description for a transition requirement.
requirement-declaration::=
invariant ∣ transition-requirement
invariant::= expr
transition-requirement::=
pre-condition “:” event “:”
(post-condition ∣ (action (“,” ∣ action)*)
∣ (post-condition “,”(action (“,” ∣ action)*)))The precondition and postcondition are logical expressions. In the transition requirement declaration, the event part can contain no more than one event (it can also benull which is a symbol showing that no event occurs), while the action part can contain multiple actions. We assume that a transition requirement contains no more than one event and actions related to the same timer.Expressions are constructed with constants, variables, and operators. Expressions have logical comparison and arithmetic operators that general programming languages such asC have. In addition, expressions in SENS have the logical implication operator (–>) and the previous state operator (~). Especially, expression   ~
v represents the previous value of  v.


### 3.3.  Semantics of SENS

ASENS specification describes requirements of an ENS consisting of subsystems communicating each other. We model the system specified by  SENS using a labeled transition system. Figure 4 illustrates our system modeling where time constraints in SENS are modeled using our timer models that will be shown later. First, each instance corresponding to a subsystem in the given specification is modeled. When the class corresponding to the subsystem contains timer variables, we compose the subsystem model and its timer models. Next, an entire ENS is modeled as a parallel composition of all subsystems. The transition system modeled from the  SENS specification is used for generating test cases and test sequences.Figure 4
A model composition for the entire ENS.In Section3.3.1, we give the modeling of timers. In Section 3.3.2, we give the modeling of a subsystem and explain the composition of the subsystem and the timer. In Section 3.3.3, we explain the composition of subsystems.


#### 3.3.1. Modeling of Timers

A timer is specified in the timer declaration with its timer name, number (time), unit, and conditions for counting up inSENS. We consider two kinds of models M
1 and M
2 for timers expressed in Figures 5(a) and 5(b). We can use simpler timer model M
2 for state elimination, while we can use timer model M
1 for considering the relation of a time length between timers (refer to Section 3.3.2.).Timer Models.
(a)
ModelM
1
(b)
ModelM
2
(c)
ModelM
2
′ for timers with multiple conditionsDefinition 2 (timer model).
We model the behavior of each timerT
i as a labeled transition system (
S
T
i
,
Σ
T
i
,
R
T
i
) with R
T
i
⊆
S
T
i
×
Σ
T
i
×
S
T
i, where S
T
i denotes a set of states, Σ
T
i denotes a set of labels, and R
T
i denotes a labeled transition for T
i. (
S
T
i
,
Σ
T
i
,
R
T
i
) for M
1 and M
2 are defined as follows: (i)
S
T
i
=
{
ready, 0, 1, …, max, over} in M
1;
(ii)
S
T
i
=
{
ready, run, over} in M
2;
(iii)
Σ
T
i
=
{
?start, ?clear, !ring, c} in M
1, M
2.In modelsM
1 and M
2, states ready and over, respectively, represent states in which timer T
i is ready and counted over. In model M
1, state “h” (0  ≤ h ≤ max) represents a state in which timer T
i has counted up h times. In model M
2, we reduce states 0, …, max to state run representing a state in which timer T
i is running, for the state elimination.In both models, each state is changed to stateready when receiving message clear. State ready is changed to state 0 in M
1 (resp., state run in M
2) when receiving message  start. State max in M
1 (resp., state run in M
2) is changed to stateover when sending message ring. We define that transitions labeled with !
s
t
a
r
t and c occur only if the condition for the timer holds. If the condition is not described in the timer declaration, the condition is considered to be “true”.If there are multiple conditionsp
,
q
,
…
,
r, we define transitions as represented in Figure 5(c). In the figure, transitions labeled with ?clear are eliminated for simplicity. In the figure, the first, second, and third transitions labeled with c occur when conditions p, q, and r, respectively, hold.


#### 3.3.2. Modeling of Subsystems

A subsystem is specified in the class declaration inS
E
N
S. For a given specification, we model the behavior of each subsystem as a labeled transition system in two steps. First, the behavior of a subsystem C
i except timers is modeled as a labeled transition system M
(
C
i
). Next, the behavior of a subsystem including timers is modeled as M
T
(
C
i
) which is a composition of M
(
C
i
) and models of the timers.Definition 3 (subsystem model).
We model the behavior of a subsystemC
i, except for its timers, as M
(
C
i
)
=
(
S
C
i
,
Σ
C
i
,
R
C
i
) with R
C
i
⊆
S
C
i
×
Σ
C
i
×
S
C
i. Given a SENS specification, the set of states S
C
i, the set of labels Σ
C
i, and the set of transitions R
C
i are obtained by Definitions 15, 16, and 17 of Appendix B.1.Example 4.
Consider the example specification of subsystemC
A in Pseudocode 1. Figure 6 illustrates the subsystem model for C
A which satisfies the specification. Given SENS specification for class A, the states are (~op=off,  op=off), (~op=off,  op=on), (~op=on,op=on), and (~op=on,  op=off) from variable op and previous state variable ~op used in the specification by Definition 15. By Definition 16, the labels are t!start, t?ring, B[1]. ch!m, and B[2].   ch!m with the events and actions used in the specification. Each transition in M
(
C
A
) satisfies the two conditions in Definition 17. For example, s
→
s
′ with s
= (~op=off,op=off) and s
′
= (~op=on,op=off) cannot be a transition of M
(
C
A
), since it does not hold the condition for previous state variables; that is, s
⊨ (op=on),  if and only if s
′
⊨ (~op=on) by Definition 17.Figure 6
An example model for systemC
A.We model the behavior of a subsystemC
i with its timers T
1
,
T
2
,
…
,
T
m as an interleaving composition of the subsystem model and timer models as follows:
(2)
M
T
(
C
i
)
=
M
(
C
i
)
∥
M
(
T
1
)
∥
M
(
T
2
)
∥
⋯
∥
M
(
T
m
)
,
where M
(
C
i
) denote the subsystem model explained in Definition 3 and M
(
T
j
) denotes the model for timer T
j (1
≤
j
≤
m) explained in Section 3.3.1. We inductively define the above model composition, that is, (1)
M
(
C
i
)
∥
M
(
T
j
) in Definition 18,
(2)
M
(
C
T
i
)
∥
M
(
T
k
) in Definition 19, where M
(
C
T
i
)
=
M
(
C
i
)
∥
M
(
T
1
)
∥
⋯
∥
M
(
T
j
) with j
<
k. And the composition rule is defined in Definitions 18 and 19 of Appendix B.2.Example 5.
Consider again the example specification of subsystemC
A in Pseudocode 1. Figure 7 shows a part of the composed model of M
(
C
A
) in Figure 6 and timer model M
2 for timer t. The transitions labeled with t
_
start and t
_
ring correspond to rules (a1) and (a2) in Definition 18, that is, message synchronization. The transition labeled with c corresponds to rule (a4) in Definition 18.Figure 7
An example model for systemC
A with a timer.


#### 3.3.3. System Model

Now we explain the model for the entire system. Assume that the entire system consists ofk subsystems. We define the model for the system as the parallel synchronized composition of labeled transition systems M
T
(
C
i
) representing all subsystems C
i (1
≤
i
≤
k). The composition of two subsystems is defined in Definition 20 and the entire system model M
T
(
C
1
)
∥
⋯
∥
M
T
(
C
n
) is obtained by an inductive composition. (When a transition of a subsystem has multiple message sending, we assume that its composition is synchronously performed in our modeling.) The composition rule is defined in the definition of Appendix B.3.Example 6.
Consider the example specifications of subsystemsC
A and C
B
[
1
] in Pseudocode 1. Figure 8 shows an example composition of transitions in M
T
(
C
A
) and M
T
(
C
B
[
1
]
).Figure 8
An example transition composition forC
A and C
B
[
1
].


## 3.1. Features of SENS

TheS
E
N
S specification is basically a set of requirements represented by logical formulas. S
E
N
S is based on a quantifier-free predicate modal logic with a next operator where predicate variables are classified into environments, systems, communication channels, and timer variables. S
E
N
S has the following features.


### 3.1.1. Property-Based

Property-based logical formulas represent requirements which constrain system behaviors. Since a part of the specification less affects the entire specification, it is easy to modify and reuseS
E
N
S specifications. A requirement is described in a traditional Hoare triple-like way:
(1)
〈
p
r
e
:
e
v
e
n
t
:
(
p
o
s
t
,
a
c
t
i
o
n
)
〉
,
where p
r
e (resp., p
o
s
t) denotes a logical constraint holding in a prestate (resp., poststate) and an e
v
e
n
t (resp., a
c
t
i
o
n) represents a message receiving (resp., sending) between subsystems. This 3-tuple requirement needs to hold for all transitions of the system model, and we call this 3-tuple requirement a transition requirement.


### 3.1.2. Test-Oriented

For a testing purpose, specifying tested values and bounds of variables is available in the variable declaration. This supports a test-oriented design and an efficient test generation fromS
E
N
S specifications.


### 3.1.3. Object-Oriented

A group of subsystems is represented as a parameterized class, and each subsystem is defined as an instance of the class in the main class representing the whole system. This representation leads to an efficient description of a large number of subsystems in an ENS.


### 3.1.4. Modular

Specifications of an ENS, a subsystem, and a function are broken down into specifications of subsystems, functions, and transition requirements, respectively. This modular construction makes it easy to specify a large-scaled and complicated ENS piece by piece and provide a reusability of specifications. This also allows a step-wise test generation fromS
E
N
S specifications for unit testing, integration testing, and system testing.


### 3.1.5. Lightweight Description of Time Constraints

We consider a timer as a component of a subsystem and then specify time constraints using events and actions with the timer.S
E
N
S provides a timer variable which is declared with a time-value, a time-unit, and a condition formula for counting up the timer.


## 3.1.1. Property-Based

Property-based logical formulas represent requirements which constrain system behaviors. Since a part of the specification less affects the entire specification, it is easy to modify and reuseS
E
N
S specifications. A requirement is described in a traditional Hoare triple-like way:
(1)
〈
p
r
e
:
e
v
e
n
t
:
(
p
o
s
t
,
a
c
t
i
o
n
)
〉
,
where p
r
e (resp., p
o
s
t) denotes a logical constraint holding in a prestate (resp., poststate) and an e
v
e
n
t (resp., a
c
t
i
o
n) represents a message receiving (resp., sending) between subsystems. This 3-tuple requirement needs to hold for all transitions of the system model, and we call this 3-tuple requirement a transition requirement.


## 3.1.2. Test-Oriented

For a testing purpose, specifying tested values and bounds of variables is available in the variable declaration. This supports a test-oriented design and an efficient test generation fromS
E
N
S specifications.


## 3.1.3. Object-Oriented

A group of subsystems is represented as a parameterized class, and each subsystem is defined as an instance of the class in the main class representing the whole system. This representation leads to an efficient description of a large number of subsystems in an ENS.


## 3.1.4. Modular

Specifications of an ENS, a subsystem, and a function are broken down into specifications of subsystems, functions, and transition requirements, respectively. This modular construction makes it easy to specify a large-scaled and complicated ENS piece by piece and provide a reusability of specifications. This also allows a step-wise test generation fromS
E
N
S specifications for unit testing, integration testing, and system testing.


## 3.1.5. Lightweight Description of Time Constraints

We consider a timer as a component of a subsystem and then specify time constraints using events and actions with the timer.S
E
N
S provides a timer variable which is declared with a time-value, a time-unit, and a condition formula for counting up the timer.


## 3.2.  Syntax of SENS

Here, we give the brief explanation ofS
E
N
S description using the following example embedded system.Example 1.
Consider an illustrating system in Figure3. There are 2 kinds of equipment, namely, classes A and B. Let us consider a simple ENS consisting of 3 subsystems A
1, B
1, and B
2, where A
1 is an instance of A and B
1 and B
2 are instances of B. A subsystem of class A sends a message m after 2 minutes from starting its operation. Each subsystem of class B turns on its lamp when receiving message m. This system can be described in the S
E
N
S specification of Pseudocode 1.Pseudocode 1:An example SENS specification.
<
main.cls>
(1)
Import  A,
B;
(2)
Class
main
(3)
Data
(4)
onoff_status  {on,off};
(5)
Var
(6)
B1,  B2 : B;
(7)
A1 : A(B1,  B2);
<A.cls>
(1)
Import B;
(2)
Extern
(3)
Data
(4)
onoff_status;  //from  main
(5)
Class  A(arg
1
: B,  arg2 : B)
(6)
Var
(7)
op
:
onoff_status{off};
(8)
Timer
(9)
t 2
min;
(10)
(11)
Function SendingM
(12)
Require
(13)
~
op==off && op==on
:
null
:
t!start;
(14)
op==on
:
t?ring
:
arg1.ch!m,
arg2.ch!m;
<B.cls>
(1)
Extern
(2)
Data
(3)
onoff_status; //from main
(4)
Class B
(5)
Data
(6)
m_type{m};
(7)
Var
(8)
op
:
onoff_status{off};
(9)
lamp
:
onoff_status{off};
(10)
Channel
(11)
ch
:
m_type;
(12)
(13)
Function Lighting
(14)
Require
(15)
op==on && lamp==off
:
ch?m
:
lamp==on;
(16)
op==off
−
> lamp==off;Figure 3
An example embedded system.TheS
E
N
S declarations consist of the following declarations (refer to Appendix A for the full syntax of SENS).(i) Main Class Declaration. File <main.cls>  specifies the main class. The main class represents the whole system consisting of subsystems and the environment. In the file <main.cls>  of Pseudocode 1, the classes A and B are imported in line 1, and subsystems A
1, B
1, and B
2 are instantiated in lines 6-7. Environment variables are declared in the Var part. Data types, environment variables, and channels declared in the main class are referred in all class declarations. Invariants (logical expressions) for the entire system are declared in the main class. In the example <main.cls>, global data type onoff_status  is declared in lines 3-4.(ii) Class Declaration. Files <A.cls>  and <B.cls>  of Pseudocode 1 specify classes A and B, respectively. A class other than the main class specifies a class of subsystems. Local data types, variables, channels, and timers for the subsystem are declared in the class declaration. In <A.cls>, local variable op and timer t are declared in lines 6–9, and a function of the subsystem is declared in lines 11–14.For data types, variables, channels, and timers externally declared and internally used, the files to declare them are imported with theImport statement and their names are described in the Extern part. The main class file is imported to all class files by default. A class can have parameters used as constants in the class specification. In line 1 of <A.cls>, class B is imported since class B is used in the parameter declaration of A. In lines 3-4, data type onoff_status is described in the Extern part.(iii) Variable and Data Type Declarations. A variable is declared with its name, type, initial value, and test declaration (values and bounds for testing) in the part following to Var. Data types are int and double with ranges, and enumerated data types are defined in the Data part. In the Data part, a type is defined as a set of values. In S
E
N
S, only finite and discrete values are used. In the example<main.cls>, a global data type, onoff_status, which has two elements on  and off, is declared in lines 3-4. In <B.cls>, a local data type, m_type, which has the only element m, is declared in lines 5-6. Using the test declaration beginning with the keywordtestedwith, one can define the specific values of variables to be considered in a testing phase. For example, consider the following variable declaration:Var v1 double  [
-2, 5
]  {0}
testedwith  {-2, 0..5   (0.5)};variablev1 is defined as follows: its type is double, its range is −2 ≤ v1 ≤ 5, its initial value 0, and its tested values are −2 and a number from 0 to 5 in increments of 0.5. In our semantics of S
E
N
S, each variable of a subsystem takes one value, that is, an element of its domain. If the declaration of a variable has a test declaration, the domain is defined by the test declaration. Otherwise, the domain is defined by the data type of the variable.(iv) Channel and Timer Declarations. Channels are used to describe communications between subsystems. A channel is declared with its name and message type. In lines 10-11 of <B.cls>, a channel ch for receiving message m is declared. A timer is declared with its name, time-value, unit, and conditions (logical formula) for counting up. When the condition is omitted, the condition is always true. For example, consider the following timer declarations:Timer
t1 5 min;
t2 5 hour [(v==dry) ∣∣ (v==cool)];Timert1 is declared to count up 5 minutes. Timer t2 is declared to count up 5 hours, but the counting is performed only when the value of v is dry or cool.The event is a message receiving (channel-name?expr) or timeout (timer-name?ring). Similarly, the action is a message sending (channel-name!expr), timer starting (timer-name!start), or timer reset (timer-name!clear). When specifying a communication between subsystems, a message sending (action) is described using both a recipient's object name and a channel name, while a message receiving (event) is described using only a channel name.(v) Function and Requirement Declarations. Functions are declared in the class declaration or in individual function declaration files. In the function declaration, constants, data types, variables, and timers can be defined locally. A function contains a set of requirements.A requirement is an expression representing an invariant or a 3-tuple of a precondition, an event, and a postcondition or/with/without actions. (More precisely, the third part of the transition requirement is a postcondition or an action or actions or a postcondition with an action or a postcondition with actions.) We call the 3-tuple requirement a transition requirement. The BNF description for a transition requirement is given in Algorithm1 (Refer to Appendix A.4).Algorithm 1:The BNF description for a transition requirement.
requirement-declaration::=
invariant ∣ transition-requirement
invariant::= expr
transition-requirement::=
pre-condition “:” event “:”
(post-condition ∣ (action (“,” ∣ action)*)
∣ (post-condition “,”(action (“,” ∣ action)*)))The precondition and postcondition are logical expressions. In the transition requirement declaration, the event part can contain no more than one event (it can also benull which is a symbol showing that no event occurs), while the action part can contain multiple actions. We assume that a transition requirement contains no more than one event and actions related to the same timer.Expressions are constructed with constants, variables, and operators. Expressions have logical comparison and arithmetic operators that general programming languages such asC have. In addition, expressions in SENS have the logical implication operator (–>) and the previous state operator (~). Especially, expression   ~
v represents the previous value of  v.


## 3.3.  Semantics of SENS

ASENS specification describes requirements of an ENS consisting of subsystems communicating each other. We model the system specified by  SENS using a labeled transition system. Figure 4 illustrates our system modeling where time constraints in SENS are modeled using our timer models that will be shown later. First, each instance corresponding to a subsystem in the given specification is modeled. When the class corresponding to the subsystem contains timer variables, we compose the subsystem model and its timer models. Next, an entire ENS is modeled as a parallel composition of all subsystems. The transition system modeled from the  SENS specification is used for generating test cases and test sequences.Figure 4
A model composition for the entire ENS.In Section3.3.1, we give the modeling of timers. In Section 3.3.2, we give the modeling of a subsystem and explain the composition of the subsystem and the timer. In Section 3.3.3, we explain the composition of subsystems.


### 3.3.1. Modeling of Timers

A timer is specified in the timer declaration with its timer name, number (time), unit, and conditions for counting up inSENS. We consider two kinds of models M
1 and M
2 for timers expressed in Figures 5(a) and 5(b). We can use simpler timer model M
2 for state elimination, while we can use timer model M
1 for considering the relation of a time length between timers (refer to Section 3.3.2.).Timer Models.
(a)
ModelM
1
(b)
ModelM
2
(c)
ModelM
2
′ for timers with multiple conditionsDefinition 2 (timer model).
We model the behavior of each timerT
i as a labeled transition system (
S
T
i
,
Σ
T
i
,
R
T
i
) with R
T
i
⊆
S
T
i
×
Σ
T
i
×
S
T
i, where S
T
i denotes a set of states, Σ
T
i denotes a set of labels, and R
T
i denotes a labeled transition for T
i. (
S
T
i
,
Σ
T
i
,
R
T
i
) for M
1 and M
2 are defined as follows: (i)
S
T
i
=
{
ready, 0, 1, …, max, over} in M
1;
(ii)
S
T
i
=
{
ready, run, over} in M
2;
(iii)
Σ
T
i
=
{
?start, ?clear, !ring, c} in M
1, M
2.In modelsM
1 and M
2, states ready and over, respectively, represent states in which timer T
i is ready and counted over. In model M
1, state “h” (0  ≤ h ≤ max) represents a state in which timer T
i has counted up h times. In model M
2, we reduce states 0, …, max to state run representing a state in which timer T
i is running, for the state elimination.In both models, each state is changed to stateready when receiving message clear. State ready is changed to state 0 in M
1 (resp., state run in M
2) when receiving message  start. State max in M
1 (resp., state run in M
2) is changed to stateover when sending message ring. We define that transitions labeled with !
s
t
a
r
t and c occur only if the condition for the timer holds. If the condition is not described in the timer declaration, the condition is considered to be “true”.If there are multiple conditionsp
,
q
,
…
,
r, we define transitions as represented in Figure 5(c). In the figure, transitions labeled with ?clear are eliminated for simplicity. In the figure, the first, second, and third transitions labeled with c occur when conditions p, q, and r, respectively, hold.


### 3.3.2. Modeling of Subsystems

A subsystem is specified in the class declaration inS
E
N
S. For a given specification, we model the behavior of each subsystem as a labeled transition system in two steps. First, the behavior of a subsystem C
i except timers is modeled as a labeled transition system M
(
C
i
). Next, the behavior of a subsystem including timers is modeled as M
T
(
C
i
) which is a composition of M
(
C
i
) and models of the timers.Definition 3 (subsystem model).
We model the behavior of a subsystemC
i, except for its timers, as M
(
C
i
)
=
(
S
C
i
,
Σ
C
i
,
R
C
i
) with R
C
i
⊆
S
C
i
×
Σ
C
i
×
S
C
i. Given a SENS specification, the set of states S
C
i, the set of labels Σ
C
i, and the set of transitions R
C
i are obtained by Definitions 15, 16, and 17 of Appendix B.1.Example 4.
Consider the example specification of subsystemC
A in Pseudocode 1. Figure 6 illustrates the subsystem model for C
A which satisfies the specification. Given SENS specification for class A, the states are (~op=off,  op=off), (~op=off,  op=on), (~op=on,op=on), and (~op=on,  op=off) from variable op and previous state variable ~op used in the specification by Definition 15. By Definition 16, the labels are t!start, t?ring, B[1]. ch!m, and B[2].   ch!m with the events and actions used in the specification. Each transition in M
(
C
A
) satisfies the two conditions in Definition 17. For example, s
→
s
′ with s
= (~op=off,op=off) and s
′
= (~op=on,op=off) cannot be a transition of M
(
C
A
), since it does not hold the condition for previous state variables; that is, s
⊨ (op=on),  if and only if s
′
⊨ (~op=on) by Definition 17.Figure 6
An example model for systemC
A.We model the behavior of a subsystemC
i with its timers T
1
,
T
2
,
…
,
T
m as an interleaving composition of the subsystem model and timer models as follows:
(2)
M
T
(
C
i
)
=
M
(
C
i
)
∥
M
(
T
1
)
∥
M
(
T
2
)
∥
⋯
∥
M
(
T
m
)
,
where M
(
C
i
) denote the subsystem model explained in Definition 3 and M
(
T
j
) denotes the model for timer T
j (1
≤
j
≤
m) explained in Section 3.3.1. We inductively define the above model composition, that is, (1)
M
(
C
i
)
∥
M
(
T
j
) in Definition 18,
(2)
M
(
C
T
i
)
∥
M
(
T
k
) in Definition 19, where M
(
C
T
i
)
=
M
(
C
i
)
∥
M
(
T
1
)
∥
⋯
∥
M
(
T
j
) with j
<
k. And the composition rule is defined in Definitions 18 and 19 of Appendix B.2.Example 5.
Consider again the example specification of subsystemC
A in Pseudocode 1. Figure 7 shows a part of the composed model of M
(
C
A
) in Figure 6 and timer model M
2 for timer t. The transitions labeled with t
_
start and t
_
ring correspond to rules (a1) and (a2) in Definition 18, that is, message synchronization. The transition labeled with c corresponds to rule (a4) in Definition 18.Figure 7
An example model for systemC
A with a timer.


### 3.3.3. System Model

Now we explain the model for the entire system. Assume that the entire system consists ofk subsystems. We define the model for the system as the parallel synchronized composition of labeled transition systems M
T
(
C
i
) representing all subsystems C
i (1
≤
i
≤
k). The composition of two subsystems is defined in Definition 20 and the entire system model M
T
(
C
1
)
∥
⋯
∥
M
T
(
C
n
) is obtained by an inductive composition. (When a transition of a subsystem has multiple message sending, we assume that its composition is synchronously performed in our modeling.) The composition rule is defined in the definition of Appendix B.3.Example 6.
Consider the example specifications of subsystemsC
A and C
B
[
1
] in Pseudocode 1. Figure 8 shows an example composition of transitions in M
T
(
C
A
) and M
T
(
C
B
[
1
]
).Figure 8
An example transition composition forC
A and C
B
[
1
].


## 3.3.1. Modeling of Timers

A timer is specified in the timer declaration with its timer name, number (time), unit, and conditions for counting up inSENS. We consider two kinds of models M
1 and M
2 for timers expressed in Figures 5(a) and 5(b). We can use simpler timer model M
2 for state elimination, while we can use timer model M
1 for considering the relation of a time length between timers (refer to Section 3.3.2.).Timer Models.
(a)
ModelM
1
(b)
ModelM
2
(c)
ModelM
2
′ for timers with multiple conditionsDefinition 2 (timer model).
We model the behavior of each timerT
i as a labeled transition system (
S
T
i
,
Σ
T
i
,
R
T
i
) with R
T
i
⊆
S
T
i
×
Σ
T
i
×
S
T
i, where S
T
i denotes a set of states, Σ
T
i denotes a set of labels, and R
T
i denotes a labeled transition for T
i. (
S
T
i
,
Σ
T
i
,
R
T
i
) for M
1 and M
2 are defined as follows: (i)
S
T
i
=
{
ready, 0, 1, …, max, over} in M
1;
(ii)
S
T
i
=
{
ready, run, over} in M
2;
(iii)
Σ
T
i
=
{
?start, ?clear, !ring, c} in M
1, M
2.In modelsM
1 and M
2, states ready and over, respectively, represent states in which timer T
i is ready and counted over. In model M
1, state “h” (0  ≤ h ≤ max) represents a state in which timer T
i has counted up h times. In model M
2, we reduce states 0, …, max to state run representing a state in which timer T
i is running, for the state elimination.In both models, each state is changed to stateready when receiving message clear. State ready is changed to state 0 in M
1 (resp., state run in M
2) when receiving message  start. State max in M
1 (resp., state run in M
2) is changed to stateover when sending message ring. We define that transitions labeled with !
s
t
a
r
t and c occur only if the condition for the timer holds. If the condition is not described in the timer declaration, the condition is considered to be “true”.If there are multiple conditionsp
,
q
,
…
,
r, we define transitions as represented in Figure 5(c). In the figure, transitions labeled with ?clear are eliminated for simplicity. In the figure, the first, second, and third transitions labeled with c occur when conditions p, q, and r, respectively, hold.


## 3.3.2. Modeling of Subsystems

A subsystem is specified in the class declaration inS
E
N
S. For a given specification, we model the behavior of each subsystem as a labeled transition system in two steps. First, the behavior of a subsystem C
i except timers is modeled as a labeled transition system M
(
C
i
). Next, the behavior of a subsystem including timers is modeled as M
T
(
C
i
) which is a composition of M
(
C
i
) and models of the timers.Definition 3 (subsystem model).
We model the behavior of a subsystemC
i, except for its timers, as M
(
C
i
)
=
(
S
C
i
,
Σ
C
i
,
R
C
i
) with R
C
i
⊆
S
C
i
×
Σ
C
i
×
S
C
i. Given a SENS specification, the set of states S
C
i, the set of labels Σ
C
i, and the set of transitions R
C
i are obtained by Definitions 15, 16, and 17 of Appendix B.1.Example 4.
Consider the example specification of subsystemC
A in Pseudocode 1. Figure 6 illustrates the subsystem model for C
A which satisfies the specification. Given SENS specification for class A, the states are (~op=off,  op=off), (~op=off,  op=on), (~op=on,op=on), and (~op=on,  op=off) from variable op and previous state variable ~op used in the specification by Definition 15. By Definition 16, the labels are t!start, t?ring, B[1]. ch!m, and B[2].   ch!m with the events and actions used in the specification. Each transition in M
(
C
A
) satisfies the two conditions in Definition 17. For example, s
→
s
′ with s
= (~op=off,op=off) and s
′
= (~op=on,op=off) cannot be a transition of M
(
C
A
), since it does not hold the condition for previous state variables; that is, s
⊨ (op=on),  if and only if s
′
⊨ (~op=on) by Definition 17.Figure 6
An example model for systemC
A.We model the behavior of a subsystemC
i with its timers T
1
,
T
2
,
…
,
T
m as an interleaving composition of the subsystem model and timer models as follows:
(2)
M
T
(
C
i
)
=
M
(
C
i
)
∥
M
(
T
1
)
∥
M
(
T
2
)
∥
⋯
∥
M
(
T
m
)
,
where M
(
C
i
) denote the subsystem model explained in Definition 3 and M
(
T
j
) denotes the model for timer T
j (1
≤
j
≤
m) explained in Section 3.3.1. We inductively define the above model composition, that is, (1)
M
(
C
i
)
∥
M
(
T
j
) in Definition 18,
(2)
M
(
C
T
i
)
∥
M
(
T
k
) in Definition 19, where M
(
C
T
i
)
=
M
(
C
i
)
∥
M
(
T
1
)
∥
⋯
∥
M
(
T
j
) with j
<
k. And the composition rule is defined in Definitions 18 and 19 of Appendix B.2.Example 5.
Consider again the example specification of subsystemC
A in Pseudocode 1. Figure 7 shows a part of the composed model of M
(
C
A
) in Figure 6 and timer model M
2 for timer t. The transitions labeled with t
_
start and t
_
ring correspond to rules (a1) and (a2) in Definition 18, that is, message synchronization. The transition labeled with c corresponds to rule (a4) in Definition 18.Figure 7
An example model for systemC
A with a timer.


## 3.3.3. System Model

Now we explain the model for the entire system. Assume that the entire system consists ofk subsystems. We define the model for the system as the parallel synchronized composition of labeled transition systems M
T
(
C
i
) representing all subsystems C
i (1
≤
i
≤
k). The composition of two subsystems is defined in Definition 20 and the entire system model M
T
(
C
1
)
∥
⋯
∥
M
T
(
C
n
) is obtained by an inductive composition. (When a transition of a subsystem has multiple message sending, we assume that its composition is synchronously performed in our modeling.) The composition rule is defined in the definition of Appendix B.3.Example 6.
Consider the example specifications of subsystemsC
A and C
B
[
1
] in Pseudocode 1. Figure 8 shows an example composition of transitions in M
T
(
C
A
) and M
T
(
C
B
[
1
]
).Figure 8
An example transition composition forC
A and C
B
[
1
].


## 4. Automatic Test Generation from the SENS Specification

In this section, we present the methods for a givenS
E
N
S specification to automatically generate test cases and test sequences in Sections 4.1 and 4.2, respectively.


### 4.1. Test Case Generation

#### 4.1.1. Concept

In our approach, we find all test cases by using a SAT solver. A SAT solver is a tool to solve the SAT (satisfiability) problem which determines whether there is a value assignment to satisfy a given Boolean formula in CNF (conjunctive normal form). Although this problem is an NP-complete problem, there have been very high-speed SAT solvers (e.g., MiniSAT [5]) for practical sized problems. Using a SAT solver, we can find distinct and enormous test cases quickly that satisfy S
E
N
S specifications.


#### 4.1.2. Test Cases

Given aS
E
N
S specification that describes a target system, every transition of the system model satisfies all requirements in the given specification, as mentioned in the previous section. Therefore, we can consider that each transition t of the system model corresponds to a one-step test case. That is, the prestate (resp., events) of t is a valid input state (resp., system inputs) of a test case and the poststate (resp., action) of t is a valid output state (resp., system output) of the test case. We formally define a test case as follows.Definition 7 (test case).
Consider a given specification𝒮. A test case is a tuple,
(3)
(
i
n
p
u
t
,
e
v
e
n
t
,
a
c
t
i
o
n
,
o
u
t
p
u
t
)
,
corresponding to a transition of the system model M such that M
⊨
𝒮. In other words, a test case is an assignment that makes every transition requirement of 𝒮 hold.Note that, if the given specification is for a subsystem module, subsystems, and an entire ENS, derived test cases are, respectively, used for unit testing, integration testing, and system testing.


#### 4.1.3. Translation of SENS to CNF

For generating test cases, we first translate all the requirements in the givenS
E
N
S specification to a CNF formula which becomes an input of a SAT solver. Since the S
E
N
S specification is a set of logical constraint formulas, we can translate it to CNF according to the semantics of S
E
N
S.There are 3 main steps of the translation procedure as follows. First, we introduce fresh propositional variables to construct the state space of the system model. Second, transition requirements and invariants in theS
E
N
S specification are translated into logical formulas. Third, we collect all of the constraints presented in logical formulas. The constraints are connected with conjunction and the result is converted to CNF. (Every propositional logic formula can be converted into an equivalent formula, that is, in CNF. However, by naive algorithms where the transformation is based on rules of De Morgan's laws and the distributive law, the size of CNF can be exponentially increased. To get a compact CNF formula, we used theTseitin-transformation  [6] after translating SENS to a propositional logic formula.) Due to space limitation, the details of all translation rules are given in Appendix C.


#### 4.1.4. Generating Test Cases

Once we obtain the CNF formula from the givenS
E
N
S specification, we apply a SAT solver to the CNF formula to find an assignment. As mentioned above, the assignment that makes requirements of the S
E
N
S specification true corresponds to a test case.Algorithm2 describes our method for generating test cases. We use a SAT solver iteratively to find all possible assignments and convert them to test cases that cover all possible transitions of the system model.Algorithm 2:Our algorithm of test case generation.
Data: A SENS specification
Result: A Set of test cases
(1)
begin
(2)
Translate the given SENS specification to a logical formula f in conjunctive normal form (CNF)
based on translation rules in Appendix C;
(3)
Input f to a SAT solver;
(4)
if
f
is  satisfiable
then
(5)    The SAT solver outputs a solution m (value assignment) corresponding to one test case;
(6)    Add the solution m to a set of solutions;
(7)    Let f
←
f
∧
¬
m and return Step  2 to search for another solution;
(8)
else
(9)     The SAT solver declares f is unsatisfiable;
(10)      Then there are no more solutions;
(11)
Translate previous solutions to test cases and stop;
(12)
return  The set of test cases;


#### 4.1.5. Filtering

The proposed method can generate all possible test cases with 100% coverage for requirements of a given specification. On the other hand, the number of complete test cases can be very huge. In order to extract efficient test cases, we also give several filtering mechanisms in our method. In the current version of our tool, a user can select test cases satisfying a precondition of transition requirements, test cases containing a communication label, and test cases whose timer label isring, which means the test cases related to a time constraint.Example 8.
Consider again the example specification of subsystemC
A in Pseudocode 1. Each transition of the model for system C
A in Figure 7 corresponds to a test case. Especially, ((~op=off,op=on), ∅, {t!start}, (~op=on,op=on)) correspond to a test case satisfying a precondition of the transition requirement <~op==off && op==on:null:t!start> in line 13 of the specification. On the other hand, ((~op=on,op=on), {t?ring}, {C_B[1].ch!m,C_B[2].ch!m}, (~op=on,op=off)) correspond to a test case containing timer label ring and communication labels.As shown in Table3, the number of all test cases for C
A is 176. Among them, test cases satisfying a precondition are 10, which is less than 6% of the entire test cases. Moreover, among them, 2 test cases can be extracted, respectively, with a communication label and timer label ring.


### 4.2. Test Sequence Generation

#### 4.2.1. Concept

As mentioned in Section4.1, our test generator can generate all possible test cases for a given S
E
N
S specification. Since the number of complete test cases can be very huge, it is hard to run tests by inputting all the test cases separately. Therefore, it is practical to extract test sequences and focus on specific variables interested for testing. To deal with this problem, we propose a test sequence generator for appropriate testing goals given by users.


#### 4.2.2. Test Sequences and Testing Goals

In our method, we generate test sequences from two inputs: given aS
E
N
S specification and a testing goal. First, we define a test sequence as follows.Definition 9 (test sequence).
A test sequence is a sequence of test cases, whose adjacent output and input are the same. This means that a test sequence is a sequence,(4)
〈
(
i
n
p
u
t
1
,
e
v
e
n
t
1
,
a
c
t
i
o
n
1
,
o
u
t
p
u
t
1
)
a
i
…
,
(
i
n
p
u
t
n
,
e
v
e
n
t
n
,
a
c
t
i
o
n
n
,
o
u
t
p
u
t
n
)
〉
,
where o
u
t
p
u
t
i
=
i
n
p
u
t
i
+
1, for i
=
1
,
…
,
n
-
1.Next, a “testing goal” is a key feature that helps to generate appropriate test sequences. This also allows us to reduce the size of space and time for searching test sequences. In the current version of our method, a user can specify the following 3 features as a testing goal: “key variables” for a testing purpose, a list of “milestone” states forming a backbone of the sequence, and a “maximum length” between two adjacent milestones. We formally define a testing goal as follows.Definition 10 (testing goals).
Given aS
E
N
S specification, a testing goal G
=
〈
V
,
S
,
L
s
〉, where V is a set of key variables, S is a list of milestone states, and L
s is a list of maximum lengths such that (1)
a “key variable” is a variable that we focus on testing in the given specification;
(2)
a “milestone” is a state that we want each test sequence to pass through;
(3)
a “maximum length,” max of a run from a milestone s
∈
S to the next milestone s
′
∈
S, denoted by s
→
≤
max
⁡
s
′, is the maximum number of transitions needed for the run.We say that a test sequence〈
(
i
1
,
e
1
,
a
1
,
o
1
)
,
…
,
(
i
n
,
e
n
,
a
n
,
o
n
)
〉 satisfies a testing goal G
=
〈
V
,
S
=
〈
s
1
,
…
,
s
k
〉
,
L
s
〉, if and only if (1) the first input state i
1 and the last output state o
n of the test sequence, respectively, are equal to the first milestone s
1 and the last milestone s
k, (2) all other milestone states exist in the input states of the test sequence in order, and (3) the length between the milestone states in the test sequence is less than the maximum length defined in L
s. In addition, value assignments only for the key variables appear in the generated test sequences satisfying the testing goal.Example 11.
If the list of milestones is〈
s
1
,
s
2
,
s
3
〉, then we can specify the maximum length in total as the →
≤
ma
x
1
·
→
≤
ma
x
2, where ma
x
1 is the maximum of transitions which can be taken to go through from the milestone s
1 to the milestone s
2, and ma
x
2 is the maximum of transitions which can be taken to go through from the milestone s
2 to the milestone s
3.
Let us consider the simple example specification of systemB in Pseudocode 1. Assume a testing goal whose key variables V = {op,lamp}, milestones S = 〈
s
1 = (op=off,lamp=off), s
2 = (op=on,lamp=on) 〉, and s
1
⟶
≤
2
s
2. Then,〈((op=off,lamp=off), ∅, ∅, (op=on,lamp=off)),((op=on,lamp=off), ch?m, ∅, (op=on,lamp=on))〉is a test sequence satisfying the testing goal.


#### 4.2.3. Generating Test Sequences

Our approach for test sequence generation has three main steps. First, from a givenS
E
N
S specification, we first generate all test cases by our method in Algorithm 2. Then, the obtained test cases correspond to all transitions of the target system model.Second, we synthesize all the transitions into a transition system (graph). Each state of this transition system is a tuple of variable assignments. Each edge is a transition relation from a prestate to a poststate, and a label of each edge is an event that makes the transition occur. The transition system of the specification is stored in a file, while the testing goal is stored in a separate file.Third, given the transition system and the testing goal in two files, we compute all possible desired test sequences that satisfy the testing goal; that is, we search the set of sequences starting from a given milestone state to another milestone state whose distance is less than the given maximum length by tree searching algorithms including exhaustive BFS (breath first search) and DFS (depth first search) algorithms. Each resulting test sequence is treated as a test scenario. In our test sequence generation, we reduce the searching state space of the system model by an equivalence partitioning based on the key variables of the given testing goal and search the sequences containing milestone states.In ourT
G
S
E
N
S, test sequences can be generated from both the original transition system and the filtered test cases. In the test sequence generation from the original transition system, the obtained test sequences obviously keep the transition relation of the original system model. In the test sequence generation from the filtered test cases, test sequences including transitions eliminated by filtering are not generated. However, since the filtering is defined by formal rules, the effect by filtering is clear for users who recognize that test sequences with filtering options will be obtained. For this reason, we believe that it does not affect the main results of our research, in other words, generations of reliable test cases/sequences.


## 4.1. Test Case Generation

### 4.1.1. Concept

In our approach, we find all test cases by using a SAT solver. A SAT solver is a tool to solve the SAT (satisfiability) problem which determines whether there is a value assignment to satisfy a given Boolean formula in CNF (conjunctive normal form). Although this problem is an NP-complete problem, there have been very high-speed SAT solvers (e.g., MiniSAT [5]) for practical sized problems. Using a SAT solver, we can find distinct and enormous test cases quickly that satisfy S
E
N
S specifications.


### 4.1.2. Test Cases

Given aS
E
N
S specification that describes a target system, every transition of the system model satisfies all requirements in the given specification, as mentioned in the previous section. Therefore, we can consider that each transition t of the system model corresponds to a one-step test case. That is, the prestate (resp., events) of t is a valid input state (resp., system inputs) of a test case and the poststate (resp., action) of t is a valid output state (resp., system output) of the test case. We formally define a test case as follows.Definition 7 (test case).
Consider a given specification𝒮. A test case is a tuple,
(3)
(
i
n
p
u
t
,
e
v
e
n
t
,
a
c
t
i
o
n
,
o
u
t
p
u
t
)
,
corresponding to a transition of the system model M such that M
⊨
𝒮. In other words, a test case is an assignment that makes every transition requirement of 𝒮 hold.Note that, if the given specification is for a subsystem module, subsystems, and an entire ENS, derived test cases are, respectively, used for unit testing, integration testing, and system testing.


### 4.1.3. Translation of SENS to CNF

For generating test cases, we first translate all the requirements in the givenS
E
N
S specification to a CNF formula which becomes an input of a SAT solver. Since the S
E
N
S specification is a set of logical constraint formulas, we can translate it to CNF according to the semantics of S
E
N
S.There are 3 main steps of the translation procedure as follows. First, we introduce fresh propositional variables to construct the state space of the system model. Second, transition requirements and invariants in theS
E
N
S specification are translated into logical formulas. Third, we collect all of the constraints presented in logical formulas. The constraints are connected with conjunction and the result is converted to CNF. (Every propositional logic formula can be converted into an equivalent formula, that is, in CNF. However, by naive algorithms where the transformation is based on rules of De Morgan's laws and the distributive law, the size of CNF can be exponentially increased. To get a compact CNF formula, we used theTseitin-transformation  [6] after translating SENS to a propositional logic formula.) Due to space limitation, the details of all translation rules are given in Appendix C.


### 4.1.4. Generating Test Cases

Once we obtain the CNF formula from the givenS
E
N
S specification, we apply a SAT solver to the CNF formula to find an assignment. As mentioned above, the assignment that makes requirements of the S
E
N
S specification true corresponds to a test case.Algorithm2 describes our method for generating test cases. We use a SAT solver iteratively to find all possible assignments and convert them to test cases that cover all possible transitions of the system model.Algorithm 2:Our algorithm of test case generation.
Data: A SENS specification
Result: A Set of test cases
(1)
begin
(2)
Translate the given SENS specification to a logical formula f in conjunctive normal form (CNF)
based on translation rules in Appendix C;
(3)
Input f to a SAT solver;
(4)
if
f
is  satisfiable
then
(5)    The SAT solver outputs a solution m (value assignment) corresponding to one test case;
(6)    Add the solution m to a set of solutions;
(7)    Let f
←
f
∧
¬
m and return Step  2 to search for another solution;
(8)
else
(9)     The SAT solver declares f is unsatisfiable;
(10)      Then there are no more solutions;
(11)
Translate previous solutions to test cases and stop;
(12)
return  The set of test cases;


### 4.1.5. Filtering

The proposed method can generate all possible test cases with 100% coverage for requirements of a given specification. On the other hand, the number of complete test cases can be very huge. In order to extract efficient test cases, we also give several filtering mechanisms in our method. In the current version of our tool, a user can select test cases satisfying a precondition of transition requirements, test cases containing a communication label, and test cases whose timer label isring, which means the test cases related to a time constraint.Example 8.
Consider again the example specification of subsystemC
A in Pseudocode 1. Each transition of the model for system C
A in Figure 7 corresponds to a test case. Especially, ((~op=off,op=on), ∅, {t!start}, (~op=on,op=on)) correspond to a test case satisfying a precondition of the transition requirement <~op==off && op==on:null:t!start> in line 13 of the specification. On the other hand, ((~op=on,op=on), {t?ring}, {C_B[1].ch!m,C_B[2].ch!m}, (~op=on,op=off)) correspond to a test case containing timer label ring and communication labels.As shown in Table3, the number of all test cases for C
A is 176. Among them, test cases satisfying a precondition are 10, which is less than 6% of the entire test cases. Moreover, among them, 2 test cases can be extracted, respectively, with a communication label and timer label ring.


## 4.1.1. Concept

In our approach, we find all test cases by using a SAT solver. A SAT solver is a tool to solve the SAT (satisfiability) problem which determines whether there is a value assignment to satisfy a given Boolean formula in CNF (conjunctive normal form). Although this problem is an NP-complete problem, there have been very high-speed SAT solvers (e.g., MiniSAT [5]) for practical sized problems. Using a SAT solver, we can find distinct and enormous test cases quickly that satisfy S
E
N
S specifications.


## 4.1.2. Test Cases

Given aS
E
N
S specification that describes a target system, every transition of the system model satisfies all requirements in the given specification, as mentioned in the previous section. Therefore, we can consider that each transition t of the system model corresponds to a one-step test case. That is, the prestate (resp., events) of t is a valid input state (resp., system inputs) of a test case and the poststate (resp., action) of t is a valid output state (resp., system output) of the test case. We formally define a test case as follows.Definition 7 (test case).
Consider a given specification𝒮. A test case is a tuple,
(3)
(
i
n
p
u
t
,
e
v
e
n
t
,
a
c
t
i
o
n
,
o
u
t
p
u
t
)
,
corresponding to a transition of the system model M such that M
⊨
𝒮. In other words, a test case is an assignment that makes every transition requirement of 𝒮 hold.Note that, if the given specification is for a subsystem module, subsystems, and an entire ENS, derived test cases are, respectively, used for unit testing, integration testing, and system testing.


## 4.1.3. Translation of SENS to CNF

For generating test cases, we first translate all the requirements in the givenS
E
N
S specification to a CNF formula which becomes an input of a SAT solver. Since the S
E
N
S specification is a set of logical constraint formulas, we can translate it to CNF according to the semantics of S
E
N
S.There are 3 main steps of the translation procedure as follows. First, we introduce fresh propositional variables to construct the state space of the system model. Second, transition requirements and invariants in theS
E
N
S specification are translated into logical formulas. Third, we collect all of the constraints presented in logical formulas. The constraints are connected with conjunction and the result is converted to CNF. (Every propositional logic formula can be converted into an equivalent formula, that is, in CNF. However, by naive algorithms where the transformation is based on rules of De Morgan's laws and the distributive law, the size of CNF can be exponentially increased. To get a compact CNF formula, we used theTseitin-transformation  [6] after translating SENS to a propositional logic formula.) Due to space limitation, the details of all translation rules are given in Appendix C.


## 4.1.4. Generating Test Cases

Once we obtain the CNF formula from the givenS
E
N
S specification, we apply a SAT solver to the CNF formula to find an assignment. As mentioned above, the assignment that makes requirements of the S
E
N
S specification true corresponds to a test case.Algorithm2 describes our method for generating test cases. We use a SAT solver iteratively to find all possible assignments and convert them to test cases that cover all possible transitions of the system model.Algorithm 2:Our algorithm of test case generation.
Data: A SENS specification
Result: A Set of test cases
(1)
begin
(2)
Translate the given SENS specification to a logical formula f in conjunctive normal form (CNF)
based on translation rules in Appendix C;
(3)
Input f to a SAT solver;
(4)
if
f
is  satisfiable
then
(5)    The SAT solver outputs a solution m (value assignment) corresponding to one test case;
(6)    Add the solution m to a set of solutions;
(7)    Let f
←
f
∧
¬
m and return Step  2 to search for another solution;
(8)
else
(9)     The SAT solver declares f is unsatisfiable;
(10)      Then there are no more solutions;
(11)
Translate previous solutions to test cases and stop;
(12)
return  The set of test cases;


## 4.1.5. Filtering

The proposed method can generate all possible test cases with 100% coverage for requirements of a given specification. On the other hand, the number of complete test cases can be very huge. In order to extract efficient test cases, we also give several filtering mechanisms in our method. In the current version of our tool, a user can select test cases satisfying a precondition of transition requirements, test cases containing a communication label, and test cases whose timer label isring, which means the test cases related to a time constraint.Example 8.
Consider again the example specification of subsystemC
A in Pseudocode 1. Each transition of the model for system C
A in Figure 7 corresponds to a test case. Especially, ((~op=off,op=on), ∅, {t!start}, (~op=on,op=on)) correspond to a test case satisfying a precondition of the transition requirement <~op==off && op==on:null:t!start> in line 13 of the specification. On the other hand, ((~op=on,op=on), {t?ring}, {C_B[1].ch!m,C_B[2].ch!m}, (~op=on,op=off)) correspond to a test case containing timer label ring and communication labels.As shown in Table3, the number of all test cases for C
A is 176. Among them, test cases satisfying a precondition are 10, which is less than 6% of the entire test cases. Moreover, among them, 2 test cases can be extracted, respectively, with a communication label and timer label ring.


## 4.2. Test Sequence Generation

### 4.2.1. Concept

As mentioned in Section4.1, our test generator can generate all possible test cases for a given S
E
N
S specification. Since the number of complete test cases can be very huge, it is hard to run tests by inputting all the test cases separately. Therefore, it is practical to extract test sequences and focus on specific variables interested for testing. To deal with this problem, we propose a test sequence generator for appropriate testing goals given by users.


### 4.2.2. Test Sequences and Testing Goals

In our method, we generate test sequences from two inputs: given aS
E
N
S specification and a testing goal. First, we define a test sequence as follows.Definition 9 (test sequence).
A test sequence is a sequence of test cases, whose adjacent output and input are the same. This means that a test sequence is a sequence,(4)
〈
(
i
n
p
u
t
1
,
e
v
e
n
t
1
,
a
c
t
i
o
n
1
,
o
u
t
p
u
t
1
)
a
i
…
,
(
i
n
p
u
t
n
,
e
v
e
n
t
n
,
a
c
t
i
o
n
n
,
o
u
t
p
u
t
n
)
〉
,
where o
u
t
p
u
t
i
=
i
n
p
u
t
i
+
1, for i
=
1
,
…
,
n
-
1.Next, a “testing goal” is a key feature that helps to generate appropriate test sequences. This also allows us to reduce the size of space and time for searching test sequences. In the current version of our method, a user can specify the following 3 features as a testing goal: “key variables” for a testing purpose, a list of “milestone” states forming a backbone of the sequence, and a “maximum length” between two adjacent milestones. We formally define a testing goal as follows.Definition 10 (testing goals).
Given aS
E
N
S specification, a testing goal G
=
〈
V
,
S
,
L
s
〉, where V is a set of key variables, S is a list of milestone states, and L
s is a list of maximum lengths such that (1)
a “key variable” is a variable that we focus on testing in the given specification;
(2)
a “milestone” is a state that we want each test sequence to pass through;
(3)
a “maximum length,” max of a run from a milestone s
∈
S to the next milestone s
′
∈
S, denoted by s
→
≤
max
⁡
s
′, is the maximum number of transitions needed for the run.We say that a test sequence〈
(
i
1
,
e
1
,
a
1
,
o
1
)
,
…
,
(
i
n
,
e
n
,
a
n
,
o
n
)
〉 satisfies a testing goal G
=
〈
V
,
S
=
〈
s
1
,
…
,
s
k
〉
,
L
s
〉, if and only if (1) the first input state i
1 and the last output state o
n of the test sequence, respectively, are equal to the first milestone s
1 and the last milestone s
k, (2) all other milestone states exist in the input states of the test sequence in order, and (3) the length between the milestone states in the test sequence is less than the maximum length defined in L
s. In addition, value assignments only for the key variables appear in the generated test sequences satisfying the testing goal.Example 11.
If the list of milestones is〈
s
1
,
s
2
,
s
3
〉, then we can specify the maximum length in total as the →
≤
ma
x
1
·
→
≤
ma
x
2, where ma
x
1 is the maximum of transitions which can be taken to go through from the milestone s
1 to the milestone s
2, and ma
x
2 is the maximum of transitions which can be taken to go through from the milestone s
2 to the milestone s
3.
Let us consider the simple example specification of systemB in Pseudocode 1. Assume a testing goal whose key variables V = {op,lamp}, milestones S = 〈
s
1 = (op=off,lamp=off), s
2 = (op=on,lamp=on) 〉, and s
1
⟶
≤
2
s
2. Then,〈((op=off,lamp=off), ∅, ∅, (op=on,lamp=off)),((op=on,lamp=off), ch?m, ∅, (op=on,lamp=on))〉is a test sequence satisfying the testing goal.


### 4.2.3. Generating Test Sequences

Our approach for test sequence generation has three main steps. First, from a givenS
E
N
S specification, we first generate all test cases by our method in Algorithm 2. Then, the obtained test cases correspond to all transitions of the target system model.Second, we synthesize all the transitions into a transition system (graph). Each state of this transition system is a tuple of variable assignments. Each edge is a transition relation from a prestate to a poststate, and a label of each edge is an event that makes the transition occur. The transition system of the specification is stored in a file, while the testing goal is stored in a separate file.Third, given the transition system and the testing goal in two files, we compute all possible desired test sequences that satisfy the testing goal; that is, we search the set of sequences starting from a given milestone state to another milestone state whose distance is less than the given maximum length by tree searching algorithms including exhaustive BFS (breath first search) and DFS (depth first search) algorithms. Each resulting test sequence is treated as a test scenario. In our test sequence generation, we reduce the searching state space of the system model by an equivalence partitioning based on the key variables of the given testing goal and search the sequences containing milestone states.In ourT
G
S
E
N
S, test sequences can be generated from both the original transition system and the filtered test cases. In the test sequence generation from the original transition system, the obtained test sequences obviously keep the transition relation of the original system model. In the test sequence generation from the filtered test cases, test sequences including transitions eliminated by filtering are not generated. However, since the filtering is defined by formal rules, the effect by filtering is clear for users who recognize that test sequences with filtering options will be obtained. For this reason, we believe that it does not affect the main results of our research, in other words, generations of reliable test cases/sequences.


## 4.2.1. Concept

As mentioned in Section4.1, our test generator can generate all possible test cases for a given S
E
N
S specification. Since the number of complete test cases can be very huge, it is hard to run tests by inputting all the test cases separately. Therefore, it is practical to extract test sequences and focus on specific variables interested for testing. To deal with this problem, we propose a test sequence generator for appropriate testing goals given by users.


## 4.2.2. Test Sequences and Testing Goals

In our method, we generate test sequences from two inputs: given aS
E
N
S specification and a testing goal. First, we define a test sequence as follows.Definition 9 (test sequence).
A test sequence is a sequence of test cases, whose adjacent output and input are the same. This means that a test sequence is a sequence,(4)
〈
(
i
n
p
u
t
1
,
e
v
e
n
t
1
,
a
c
t
i
o
n
1
,
o
u
t
p
u
t
1
)
a
i
…
,
(
i
n
p
u
t
n
,
e
v
e
n
t
n
,
a
c
t
i
o
n
n
,
o
u
t
p
u
t
n
)
〉
,
where o
u
t
p
u
t
i
=
i
n
p
u
t
i
+
1, for i
=
1
,
…
,
n
-
1.Next, a “testing goal” is a key feature that helps to generate appropriate test sequences. This also allows us to reduce the size of space and time for searching test sequences. In the current version of our method, a user can specify the following 3 features as a testing goal: “key variables” for a testing purpose, a list of “milestone” states forming a backbone of the sequence, and a “maximum length” between two adjacent milestones. We formally define a testing goal as follows.Definition 10 (testing goals).
Given aS
E
N
S specification, a testing goal G
=
〈
V
,
S
,
L
s
〉, where V is a set of key variables, S is a list of milestone states, and L
s is a list of maximum lengths such that (1)
a “key variable” is a variable that we focus on testing in the given specification;
(2)
a “milestone” is a state that we want each test sequence to pass through;
(3)
a “maximum length,” max of a run from a milestone s
∈
S to the next milestone s
′
∈
S, denoted by s
→
≤
max
⁡
s
′, is the maximum number of transitions needed for the run.We say that a test sequence〈
(
i
1
,
e
1
,
a
1
,
o
1
)
,
…
,
(
i
n
,
e
n
,
a
n
,
o
n
)
〉 satisfies a testing goal G
=
〈
V
,
S
=
〈
s
1
,
…
,
s
k
〉
,
L
s
〉, if and only if (1) the first input state i
1 and the last output state o
n of the test sequence, respectively, are equal to the first milestone s
1 and the last milestone s
k, (2) all other milestone states exist in the input states of the test sequence in order, and (3) the length between the milestone states in the test sequence is less than the maximum length defined in L
s. In addition, value assignments only for the key variables appear in the generated test sequences satisfying the testing goal.Example 11.
If the list of milestones is〈
s
1
,
s
2
,
s
3
〉, then we can specify the maximum length in total as the →
≤
ma
x
1
·
→
≤
ma
x
2, where ma
x
1 is the maximum of transitions which can be taken to go through from the milestone s
1 to the milestone s
2, and ma
x
2 is the maximum of transitions which can be taken to go through from the milestone s
2 to the milestone s
3.
Let us consider the simple example specification of systemB in Pseudocode 1. Assume a testing goal whose key variables V = {op,lamp}, milestones S = 〈
s
1 = (op=off,lamp=off), s
2 = (op=on,lamp=on) 〉, and s
1
⟶
≤
2
s
2. Then,〈((op=off,lamp=off), ∅, ∅, (op=on,lamp=off)),((op=on,lamp=off), ch?m, ∅, (op=on,lamp=on))〉is a test sequence satisfying the testing goal.


## 4.2.3. Generating Test Sequences

Our approach for test sequence generation has three main steps. First, from a givenS
E
N
S specification, we first generate all test cases by our method in Algorithm 2. Then, the obtained test cases correspond to all transitions of the target system model.Second, we synthesize all the transitions into a transition system (graph). Each state of this transition system is a tuple of variable assignments. Each edge is a transition relation from a prestate to a poststate, and a label of each edge is an event that makes the transition occur. The transition system of the specification is stored in a file, while the testing goal is stored in a separate file.Third, given the transition system and the testing goal in two files, we compute all possible desired test sequences that satisfy the testing goal; that is, we search the set of sequences starting from a given milestone state to another milestone state whose distance is less than the given maximum length by tree searching algorithms including exhaustive BFS (breath first search) and DFS (depth first search) algorithms. Each resulting test sequence is treated as a test scenario. In our test sequence generation, we reduce the searching state space of the system model by an equivalence partitioning based on the key variables of the given testing goal and search the sequences containing milestone states.In ourT
G
S
E
N
S, test sequences can be generated from both the original transition system and the filtered test cases. In the test sequence generation from the original transition system, the obtained test sequences obviously keep the transition relation of the original system model. In the test sequence generation from the filtered test cases, test sequences including transitions eliminated by filtering are not generated. However, since the filtering is defined by formal rules, the effect by filtering is clear for users who recognize that test sequences with filtering options will be obtained. For this reason, we believe that it does not affect the main results of our research, in other words, generations of reliable test cases/sequences.


## 5. Implementation and Experiments

### 5.1. Implementation

We implemented our approach ofS
E
N
S-based automatic test generation in the tool called T
G
S
E
N
S. The tool T
G
S
E
N
S consists of the following four parts as illustrated in Figure 2. (1) The first part translates the specification written in S
E
N
S into a CNF formula. (2) The second part searches and collects all assignments that satisfy the CNF formula by using a SAT solver as its core engine. (3) The third part translates the obtained assignments into test cases which are expressed with variables used in the original S
E
N
S specification. (4) The forth part searches the test sequences from the output file of the third part and given testing goals. The resulting test sequences can be viewed by two ways: a textual format or a graphical figure using a dot file viewer.Currently, for the function level (corresponding to the function declaration inS
E
N
S) and the subsystem level (corresponding to the class declaration in S
E
N
S), we have completed the implementation of the first part in T
G
S
E
N
S but not yet for the system level. That means that the implementation for the composition of subsystems for the entire system level is our future work. Hence, the current version of our tool can perform the test generation for unit testing.Our tool was implemented on Windows XP for both ×86 and ×64 environments. The first, third, and forth parts were implemented with a Java language. The second part was implemented based on MiniSAT [5] with  C++. The size of the implemented programs is totally about 20,000 lines, respectively, 16,000, 3,000, 500, and 340 lines for each part.We also implemented the user interface (in Japanese) ofT
G
S
E
N
S given in Figure 9. Given an input S
E
N
S specification, our tool has execution options to generate output files of exhaustive test cases, filtered test cases, and test sequences under a given testing goal. T
G
S
E
N
S also has a function to check a reachability of states and generate path sequences among the input states.The GUI interface ofT
G
S
E
N
S.
(a)
The main interface for generating test cases.
(b)
The interface for generating test sequences.


### 5.2. Experiments: Specification in SENS

We appliedS
E
N
S to specify system requirements of real air-conditioning systems by Company D. In general, there are specifications with different levels. In Company D, specifications are divided into “instruction manuals,” “functional specifications,” and “detailed specifications,” and each specification is broken into functions. For example, as to specifications of certain indoor equipment, an instruction manual consists of about 10 functions with 30 pages, and a functional specification and a detailed specification, respectively, consist of about 80 functions with 400 pages.We translated several specifications in a natural language with tables and figures toS
E
N
S specifications. The target specifications were for two modules F
h and F
i in an instruction manual and one function F
j in a detailed specification of an indoor equipment, one function F
l in a functional specification of an air-cleaning system, and three functions F
m, F
n, and F
o in a functional specification of a controller.For all specifications, this translation needed 1 or 2 days by one person who is one of ourS
E
N
S developers. Almost all (70–80%) of the translation time was for understanding the real specifications and confirming whether the S
E
N
S specifications are valid with industrial engineers, while the rest of the time (several hours) was for the actual description. In addition, we held a one-day seminar for industrial engineers to explain how to describe the S
E
N
S specifications and we confirmed that after the one-day seminar, the engineers were easily able to use S
E
N
S to specify embedded systems by themselves.Example 12.
We show a part of an exampleS
E
N
S specification for function F
l in Pseudocode 2. F
l is a mode change function for an air-cleaning system by Company D. The original specification of this function was written in Japanese with A
4 sized 4 pages and includes 5 tables and 4 transition diagrams. We transformed this document into about 100 lines of a S
E
N
S specification. The S
E
N
S specification consists of 8 variables (including 6 global variables, 1 local variable, and 1 channel), 20 invariants, and 8 transition specifications. Lines 16–18 specify invariants and lines 20–22 specify transition specifications. All 8 variables have discrete values and the details of variables and their ranges are given in Table 1.Table 1
Variables in the example specification for functionF
l.
Variable
Variable description
Range
M
ode_A
Mode of operation
6
Mode_B
Mode of humidity
4
AV
Actual air volume
7
AP
Air purity
5
BM
Brightness for monitor LED
3
BO
Brightness for other LED
3
BU
User-defined brightness
3
C
Channel for indicating pushing a button
3Pseudocode 2:An example SENS specification for an air-cleaning system
<
AC.cls>
(1)
C
lass AC
(2)
Data
(3)
Type_opMode  {Off, Auto, Turbo, Pollen, Calm, Normal};
(4)
Type_humidMode
{Off, Auto, Cont, High};
(5)
Type_airVolume
{W0, W1, W2, W3, W4, W5, W6};
(6)
Type_airPurity
{KTY1, KTY2, KTY3, KTY4, KTY5};
(7)
Type_Brightness
{Normal, Dark, Off};
(8)
Type_switch
{On};
(9)
Var
(10)
Mode_A: Type_opMode; //Mode of operation
(11)
Mode_B: Type_humidMode; //Mode of humidity
(12)
AV
:
Type_airVolume; //Actual air volume
(13)
AP
:
Type_airPurity; //
Air purity
(14)
BM
:
Type_Brightness; //Brightness for monitor LED
(15)
BO
:
Type_Brightness; //Brightness for other LED
(16)
Channel
(17)
C
:
Type_switch; //Indicating pushing a button
(18)
⋯
<Mode_Change.func>
(1)
Bundled AC;
(2)
Extern
(3)
Data
(4)
Type_opMode, Type_humidMode,
(5)
Type_airVolume, Type_airPurity,
(6)
Type_Brightness, Type_switch;
(7)
Var
(8)
Mode_A, Mode_B, AV, AP, BM, BO;
(9)
Channel
(10)
C;
(11)
(12)  Function Mode_Change
(13)  Var
(14)   BU
:
Type_Brightness; //User
-
defined brightness
(15)  Require
(16)
Mode_A==Auto
−
> (AV==W
1  ∣
∣  AV==W2  ∣
∣  AV==W3  ∣
∣  AV==W4  ∣∣
AV==W5);
(17)
Mode_A==Auto && Mode_B==Off && AP==KTY1
−
> AV==W1;
(18)
Mode_A==Calm
−
> AV==W1;
(19)    ⋯
(20)
M
ode_A!=Off && BU==Normal: C?On
:
BU==Dark;
(21)
M
ode_A!=Off && BU==Dark: C?On
:
BU==Off;
(22)
true
:
C?On
:
Mode_A==
~
Mode_A;
(23)
⋯Table2 shows the scale of the S
E
N
S specifications for function F
h
-
F
o: the number of lines except comments and blank lines, the number of declared variables and channels, and the number of requirements including invariants and transition requirements. As to the specification of F
o, the size of requirements was relatively long since variables of the array type with a big size are used. In the future, our S
E
N
S description could be more compact by preparing for-statement or while-statement descriptions. For comparison, we also show the number of pages of the original specifications in a natural language in Table 2.Table 2
Scales of exampleSENS specifications.
System
Function
SENS Spec.
Original spec.
Number of lines
Number of variables
Number of req.
Number of pages
Indoor equip.
F
h
12
5
7
1
Indoor equip.
F
i
22
4
6
1
Indoor equip.
F
j
71
6
22
2
Air cleaner
F
l
101
7
28
4
Controller
F
m
77
6
22
3
Controller
F
n
52
6
4
4
Controller
F
o
428
10
47
4Table 3
Experiment results for test case generation.
Systemfunction
SENS Spec.
CNF
Test cases
Execution times (sec.)
Number of  states
Number of trans. labels
Number ofliterals
Number of  clauses
Number oftest cases
SENS to CNF
Search allassignments
Translate to testcases
A
12
17
25
68
176
0.044
0.031
0.056
B
4
3
11
19
19
0.050
0.006
0.013
F
i
12
36
36
141
1,330
0.069
0.053
0.125
F
j
≈
7.2
×
1
0
10
30
620
62,845
893,155
0.175
1565.90
56.57
F
k
4.5
×
1
0
4
30
102
406
157,874
0.078
62.24
21.77
F
l
≈
6.8
×
1
0
4
3
91
715
77,700
0.151
9.609
1.929Although we, here, showed the experimental results only for air-conditioning systems, we also have other case studies applyingS
E
N
S to specify embedded systems such as an electric pot and an automatic dispenser. For instance, we applied S
E
N
S to describe a requirement specification for an electric pot (http://www.sessame.jp/workinggroup/WorkingGroup2/POT_Specification.htm), which has been openly used as an example embedded system by SESSAME (http://www.sessame.jp) (Society of Embedded Software Skill Acquisition for Managers and Engineers) of Japan. The original requirement specification was written in Japanese including state transition diagrams with 14 pages and consisting of 14 functions. We described approximately 1,100 lines of the SENS specifications for all the functions, which include 28 variables, 5 timers, and 7 channels in the class specification and totally 386 requirements for all function specifications. Through our case studies, we confirmed that S
E
N
S is efficiently applicable to not only the air-conditioning systems but also other general embedded systems.In addition, by describing the specifications inS
E
N
S, we found several undefined and under-specified requirements in the original specifications for the target air-conditioning system. Through the feasibility study, we could confirm both the description ability and facility of S
E
N
S. Engineers in Company D plan to use our tool in real development processes. We anticipate that using S
E
N
S increases the quality of specifications by preventing the undefinition, the ambiguity, and the inconsistency in the specifications.


### 5.3. Experiments: Test Generation

In this section, we describe several case studies of generating test cases and test sequences from given example specifications<A.cls> and <B.cls> in Pseudocode 1 and F
i, F
j, F
k, and F
l, using our tool T
G
S
E
N
S. F
k is a specification whose variable range is reduced from that of F
j for testing. The experiment was performed in the following environments: Intel Core 2 Duo P8600 2.4 GHz, 3.0 GB Memory, Microsoft Windows XP SP3, and Sun Java Runtime Environment 1.6.0_24.Table3 describes the result of applying T
G
S
E
N
S to test case generation. In the table, we show the size of S
E
N
S specifications, the size of CNF, the number of test cases, and the execution times to generate test cases for each part of T
G
S
E
N
S. For the size of a SENS specification, we represent the number of states and the number of transition labels in the table. Here, the number of states indicates the one of the state space constructed by all possible variable assignments in the specification. The number of transition labels indicates the number of labels in the system model constructed from the specification.Example 13.
Consider the case ofF
l. The number of possible states (including states not satisfying the specification) for F
l is 6
×
4
×
7
×
5
×
3
3
= 68,040 from Table 1. The number of transition labels is 2 as shown in Table 3. Then the number of all possible state transitions (those that do not satisfy the specification are included) is 68,040
×
2
×
68,040
≈
9.3
×
1
0
9. From such a large number of transitions, T
G
S
E
N
S figured out 77,700 transitions satisfying the given specification as test cases within 12 seconds. For instance, as for the filtering option of including a communication label, T
G
S
E
N
S selected 8,100 test cases (≈10.5% of all the test cases) within 1 second.ForF
j (resp., F
k), T
G
S
E
N
S took only about 26 (resp., 1) minutes to generate approximately 900,000 (resp., 160,000) test cases. For example, the specification of F
j has 13 variables including 3 previous state variables and those value ranges are 3, 5, 5, 4, 5, 5, 2, 3
5, 3
5, 3, 3, 3, and 3. Then, the number of states for F
j is 2
×
3
15
×
4
×
5
4
=
71,744,535,000
≈
7.2
×
1
0
10. On the other hand, the numbers of states for F
k and F
l are 45,000 and 68,040, respectively. F
j has a feature of including variables whose range are large, like 3
5, and thus the number of states is excessively large compared to those of other specifications. The execution result of F
j indicates that the specification has 71,744,535,000
≈
7.2
×
1
0
10 states and 30 transition labels. Then, the number of all possible state transitions for F
j is 71,744,535,000
×
30
×
71,744,535,000
≈
1.5
×
1
0
23. Since the number of state transitions for F
j is much larger than those for F
k and F
l, the CNF size for F
j is much larger than those for F
k and F
l. Accordingly, F
j needed much execution time to search test cases. Although, with such a huge amount of state space, it is very impossible to manually check all cases by human, T
G
S
E
N
S can correctly do that and takes only about 26 minutes.We next describe the result of applyingT
G
S
E
N
S to test sequence generation. Table 4 shows the results using the S
E
N
S specification for function F
l with 3 example testing goals, G1–G3. In the table, for each testing goal, we show the number of milestone states, the maximum lengths between milestones, the number of key variables of the given testing goal, the number of test sequences, and the execution time to generate test sequences.Table 4
Experiment results for test sequence generation.
Number of sequences
Exe. time
(1)
(2)
(3)
G1
1
2
·
→
≤
2
·
25
1.3 sec.
G2
1
2
·
→
≤
3
·
156
8 min.
G3
3
3
·
→
≤
2
·
→
≤
2
·
896
3 min.
(1) Number of key variables, (2) number of milestones, and (3) Maximum lengths.Example 14.
Pseudocode3 shows the input file to specify the testing goal G3 in T
G
S
E
N
S. We can also set the testing goal directly in the GUI interface of T
G
S
E
N
S shown in Figure 9(b). The testing goal G3 specifies the following: (i)
key variables (declared in lines 25–28): three variablesMode_A, Mode_B,  and AVin the specification.
(ii)
The list of milestones (declared in lines 4–19):〈
s
1
,
s
2
,
s
3
〉, where s
1 is a state in which Mode_A=Auto, s
2 is a state in which Mode_A=Off, and s
3 is a state in which Mode_A=Auto.
(iii)
maximum lengths between milestones (declared in lines 22-23):s
1
→
≤
2
s
2 and s
2
→
≤
2
s
3.
When the specification forF
l and the testing goal G3 are given, a transition system of this function is first obtained from the result of test case generation. Then, T
G
S
E
N
S automatically searches desired test sequences satisfying the testing goal from the transition system. Pseudocode 4 shows a part of the generated test sequences.
The resulting transition system forF
l has 1,800 states and 77,700 transitions. From the transition system, T
G
S
E
N
S figured out 28 (resp., 32) sequences from s
1 to s
2 (resp., s
2 to s
3) and thus totally 896 (=28 × 32) test sequences satisfying the testing goal only in 3 minutes.Pseudocode 3:An example testing goal.
(
1)
[
AllTransitionFileName
]
(2)
mode_op2.csv;
(3)
(4)
//
Milestone List
(5)      [
MilestoneList
]
(6)    //
first Milestone
(7)   AC::Mode_A#Auto,
(8)   AC::AV#W3,
(9)
AC::AP#KTY3,
(10)
AC::Mode_B#Auto,
(11)
AC::Mode_Change::BU#
Normal,
(12)
AC::BM#Normal,
(13)
AC::BO#Normal;
(14)
(15)
//
second Milestone
(16)
AC::Mode_A#Off;
(17)
(18)
//
third Milestone
(19)
AC::Mode_A#Auto;
(20)
(21)
//
maximum lengths
between two milestones
(22)
[
StepNumList
]
(23)
2,2;
(24)
(25)
[
SelectVarNameList
]
(26)
AC::Mode_A,
(27)
AC::AV,
(28)
AC::Mode_B;Pseudocode 4:An example output: Test sequences.
[
Trace: 0
]
[
AC::Mode_B#Auto, AC::Mode_A#Auto, AC::AV#W3
]
[
AC::Mode_B#Cont, AC::Mode_A#Auto, AC::AV#W1
]
[
AC::Mode_B#Off, AC::Mode_A#Off, AC::AV#W0
]
[
AC::Mode_B#Off, AC::Mode_A#Auto, AC::AV#W1
]
[
AC::Mode_B#High, AC::Mode_A#Auto, AC::AV#W1
]
[
Trace: 1
]
[
AC::Mode_B#Auto, AC::Mode_A#Auto, AC::AV#W3
]
[
AC::Mode_B#Cont, AC::Mode_A#Auto, AC::AV#W1
]
[
AC::Mode_B#Off, AC::Mode_A#Off, AC::AV#W0
]
[
AC::Mode_B#Off, AC::Mode_A#Auto, AC::AV#W3
]
[
AC::Mode_B#High, AC::Mode_A#Auto, AC::AV#W1
]
[
Trace: 2
]
[
AC::Mode_B#Auto, AC::Mode_A#Auto, AC::AV#W3
]
[
AC::Mode_B#Cont, AC::Mode_A#Auto, AC::AV#W1
]
[
AC::Mode_B#Off, AC::Mode_A#Off, AC::AV#W0
]
[
AC::Mode_B#Off, AC::Mode_A#Auto, AC::AV#W2
]
[
AC::Mode_B#High, AC::Mode_A#Auto, AC::AV#W1
]
⋯


## 5.1. Implementation

We implemented our approach ofS
E
N
S-based automatic test generation in the tool called T
G
S
E
N
S. The tool T
G
S
E
N
S consists of the following four parts as illustrated in Figure 2. (1) The first part translates the specification written in S
E
N
S into a CNF formula. (2) The second part searches and collects all assignments that satisfy the CNF formula by using a SAT solver as its core engine. (3) The third part translates the obtained assignments into test cases which are expressed with variables used in the original S
E
N
S specification. (4) The forth part searches the test sequences from the output file of the third part and given testing goals. The resulting test sequences can be viewed by two ways: a textual format or a graphical figure using a dot file viewer.Currently, for the function level (corresponding to the function declaration inS
E
N
S) and the subsystem level (corresponding to the class declaration in S
E
N
S), we have completed the implementation of the first part in T
G
S
E
N
S but not yet for the system level. That means that the implementation for the composition of subsystems for the entire system level is our future work. Hence, the current version of our tool can perform the test generation for unit testing.Our tool was implemented on Windows XP for both ×86 and ×64 environments. The first, third, and forth parts were implemented with a Java language. The second part was implemented based on MiniSAT [5] with  C++. The size of the implemented programs is totally about 20,000 lines, respectively, 16,000, 3,000, 500, and 340 lines for each part.We also implemented the user interface (in Japanese) ofT
G
S
E
N
S given in Figure 9. Given an input S
E
N
S specification, our tool has execution options to generate output files of exhaustive test cases, filtered test cases, and test sequences under a given testing goal. T
G
S
E
N
S also has a function to check a reachability of states and generate path sequences among the input states.The GUI interface ofT
G
S
E
N
S.
(a)
The main interface for generating test cases.
(b)
The interface for generating test sequences.


## 5.2. Experiments: Specification in SENS

We appliedS
E
N
S to specify system requirements of real air-conditioning systems by Company D. In general, there are specifications with different levels. In Company D, specifications are divided into “instruction manuals,” “functional specifications,” and “detailed specifications,” and each specification is broken into functions. For example, as to specifications of certain indoor equipment, an instruction manual consists of about 10 functions with 30 pages, and a functional specification and a detailed specification, respectively, consist of about 80 functions with 400 pages.We translated several specifications in a natural language with tables and figures toS
E
N
S specifications. The target specifications were for two modules F
h and F
i in an instruction manual and one function F
j in a detailed specification of an indoor equipment, one function F
l in a functional specification of an air-cleaning system, and three functions F
m, F
n, and F
o in a functional specification of a controller.For all specifications, this translation needed 1 or 2 days by one person who is one of ourS
E
N
S developers. Almost all (70–80%) of the translation time was for understanding the real specifications and confirming whether the S
E
N
S specifications are valid with industrial engineers, while the rest of the time (several hours) was for the actual description. In addition, we held a one-day seminar for industrial engineers to explain how to describe the S
E
N
S specifications and we confirmed that after the one-day seminar, the engineers were easily able to use S
E
N
S to specify embedded systems by themselves.Example 12.
We show a part of an exampleS
E
N
S specification for function F
l in Pseudocode 2. F
l is a mode change function for an air-cleaning system by Company D. The original specification of this function was written in Japanese with A
4 sized 4 pages and includes 5 tables and 4 transition diagrams. We transformed this document into about 100 lines of a S
E
N
S specification. The S
E
N
S specification consists of 8 variables (including 6 global variables, 1 local variable, and 1 channel), 20 invariants, and 8 transition specifications. Lines 16–18 specify invariants and lines 20–22 specify transition specifications. All 8 variables have discrete values and the details of variables and their ranges are given in Table 1.Table 1
Variables in the example specification for functionF
l.
Variable
Variable description
Range
M
ode_A
Mode of operation
6
Mode_B
Mode of humidity
4
AV
Actual air volume
7
AP
Air purity
5
BM
Brightness for monitor LED
3
BO
Brightness for other LED
3
BU
User-defined brightness
3
C
Channel for indicating pushing a button
3Pseudocode 2:An example SENS specification for an air-cleaning system
<
AC.cls>
(1)
C
lass AC
(2)
Data
(3)
Type_opMode  {Off, Auto, Turbo, Pollen, Calm, Normal};
(4)
Type_humidMode
{Off, Auto, Cont, High};
(5)
Type_airVolume
{W0, W1, W2, W3, W4, W5, W6};
(6)
Type_airPurity
{KTY1, KTY2, KTY3, KTY4, KTY5};
(7)
Type_Brightness
{Normal, Dark, Off};
(8)
Type_switch
{On};
(9)
Var
(10)
Mode_A: Type_opMode; //Mode of operation
(11)
Mode_B: Type_humidMode; //Mode of humidity
(12)
AV
:
Type_airVolume; //Actual air volume
(13)
AP
:
Type_airPurity; //
Air purity
(14)
BM
:
Type_Brightness; //Brightness for monitor LED
(15)
BO
:
Type_Brightness; //Brightness for other LED
(16)
Channel
(17)
C
:
Type_switch; //Indicating pushing a button
(18)
⋯
<Mode_Change.func>
(1)
Bundled AC;
(2)
Extern
(3)
Data
(4)
Type_opMode, Type_humidMode,
(5)
Type_airVolume, Type_airPurity,
(6)
Type_Brightness, Type_switch;
(7)
Var
(8)
Mode_A, Mode_B, AV, AP, BM, BO;
(9)
Channel
(10)
C;
(11)
(12)  Function Mode_Change
(13)  Var
(14)   BU
:
Type_Brightness; //User
-
defined brightness
(15)  Require
(16)
Mode_A==Auto
−
> (AV==W
1  ∣
∣  AV==W2  ∣
∣  AV==W3  ∣
∣  AV==W4  ∣∣
AV==W5);
(17)
Mode_A==Auto && Mode_B==Off && AP==KTY1
−
> AV==W1;
(18)
Mode_A==Calm
−
> AV==W1;
(19)    ⋯
(20)
M
ode_A!=Off && BU==Normal: C?On
:
BU==Dark;
(21)
M
ode_A!=Off && BU==Dark: C?On
:
BU==Off;
(22)
true
:
C?On
:
Mode_A==
~
Mode_A;
(23)
⋯Table2 shows the scale of the S
E
N
S specifications for function F
h
-
F
o: the number of lines except comments and blank lines, the number of declared variables and channels, and the number of requirements including invariants and transition requirements. As to the specification of F
o, the size of requirements was relatively long since variables of the array type with a big size are used. In the future, our S
E
N
S description could be more compact by preparing for-statement or while-statement descriptions. For comparison, we also show the number of pages of the original specifications in a natural language in Table 2.Table 2
Scales of exampleSENS specifications.
System
Function
SENS Spec.
Original spec.
Number of lines
Number of variables
Number of req.
Number of pages
Indoor equip.
F
h
12
5
7
1
Indoor equip.
F
i
22
4
6
1
Indoor equip.
F
j
71
6
22
2
Air cleaner
F
l
101
7
28
4
Controller
F
m
77
6
22
3
Controller
F
n
52
6
4
4
Controller
F
o
428
10
47
4Table 3
Experiment results for test case generation.
Systemfunction
SENS Spec.
CNF
Test cases
Execution times (sec.)
Number of  states
Number of trans. labels
Number ofliterals
Number of  clauses
Number oftest cases
SENS to CNF
Search allassignments
Translate to testcases
A
12
17
25
68
176
0.044
0.031
0.056
B
4
3
11
19
19
0.050
0.006
0.013
F
i
12
36
36
141
1,330
0.069
0.053
0.125
F
j
≈
7.2
×
1
0
10
30
620
62,845
893,155
0.175
1565.90
56.57
F
k
4.5
×
1
0
4
30
102
406
157,874
0.078
62.24
21.77
F
l
≈
6.8
×
1
0
4
3
91
715
77,700
0.151
9.609
1.929Although we, here, showed the experimental results only for air-conditioning systems, we also have other case studies applyingS
E
N
S to specify embedded systems such as an electric pot and an automatic dispenser. For instance, we applied S
E
N
S to describe a requirement specification for an electric pot (http://www.sessame.jp/workinggroup/WorkingGroup2/POT_Specification.htm), which has been openly used as an example embedded system by SESSAME (http://www.sessame.jp) (Society of Embedded Software Skill Acquisition for Managers and Engineers) of Japan. The original requirement specification was written in Japanese including state transition diagrams with 14 pages and consisting of 14 functions. We described approximately 1,100 lines of the SENS specifications for all the functions, which include 28 variables, 5 timers, and 7 channels in the class specification and totally 386 requirements for all function specifications. Through our case studies, we confirmed that S
E
N
S is efficiently applicable to not only the air-conditioning systems but also other general embedded systems.In addition, by describing the specifications inS
E
N
S, we found several undefined and under-specified requirements in the original specifications for the target air-conditioning system. Through the feasibility study, we could confirm both the description ability and facility of S
E
N
S. Engineers in Company D plan to use our tool in real development processes. We anticipate that using S
E
N
S increases the quality of specifications by preventing the undefinition, the ambiguity, and the inconsistency in the specifications.


## 5.3. Experiments: Test Generation

In this section, we describe several case studies of generating test cases and test sequences from given example specifications<A.cls> and <B.cls> in Pseudocode 1 and F
i, F
j, F
k, and F
l, using our tool T
G
S
E
N
S. F
k is a specification whose variable range is reduced from that of F
j for testing. The experiment was performed in the following environments: Intel Core 2 Duo P8600 2.4 GHz, 3.0 GB Memory, Microsoft Windows XP SP3, and Sun Java Runtime Environment 1.6.0_24.Table3 describes the result of applying T
G
S
E
N
S to test case generation. In the table, we show the size of S
E
N
S specifications, the size of CNF, the number of test cases, and the execution times to generate test cases for each part of T
G
S
E
N
S. For the size of a SENS specification, we represent the number of states and the number of transition labels in the table. Here, the number of states indicates the one of the state space constructed by all possible variable assignments in the specification. The number of transition labels indicates the number of labels in the system model constructed from the specification.Example 13.
Consider the case ofF
l. The number of possible states (including states not satisfying the specification) for F
l is 6
×
4
×
7
×
5
×
3
3
= 68,040 from Table 1. The number of transition labels is 2 as shown in Table 3. Then the number of all possible state transitions (those that do not satisfy the specification are included) is 68,040
×
2
×
68,040
≈
9.3
×
1
0
9. From such a large number of transitions, T
G
S
E
N
S figured out 77,700 transitions satisfying the given specification as test cases within 12 seconds. For instance, as for the filtering option of including a communication label, T
G
S
E
N
S selected 8,100 test cases (≈10.5% of all the test cases) within 1 second.ForF
j (resp., F
k), T
G
S
E
N
S took only about 26 (resp., 1) minutes to generate approximately 900,000 (resp., 160,000) test cases. For example, the specification of F
j has 13 variables including 3 previous state variables and those value ranges are 3, 5, 5, 4, 5, 5, 2, 3
5, 3
5, 3, 3, 3, and 3. Then, the number of states for F
j is 2
×
3
15
×
4
×
5
4
=
71,744,535,000
≈
7.2
×
1
0
10. On the other hand, the numbers of states for F
k and F
l are 45,000 and 68,040, respectively. F
j has a feature of including variables whose range are large, like 3
5, and thus the number of states is excessively large compared to those of other specifications. The execution result of F
j indicates that the specification has 71,744,535,000
≈
7.2
×
1
0
10 states and 30 transition labels. Then, the number of all possible state transitions for F
j is 71,744,535,000
×
30
×
71,744,535,000
≈
1.5
×
1
0
23. Since the number of state transitions for F
j is much larger than those for F
k and F
l, the CNF size for F
j is much larger than those for F
k and F
l. Accordingly, F
j needed much execution time to search test cases. Although, with such a huge amount of state space, it is very impossible to manually check all cases by human, T
G
S
E
N
S can correctly do that and takes only about 26 minutes.We next describe the result of applyingT
G
S
E
N
S to test sequence generation. Table 4 shows the results using the S
E
N
S specification for function F
l with 3 example testing goals, G1–G3. In the table, for each testing goal, we show the number of milestone states, the maximum lengths between milestones, the number of key variables of the given testing goal, the number of test sequences, and the execution time to generate test sequences.Table 4
Experiment results for test sequence generation.
Number of sequences
Exe. time
(1)
(2)
(3)
G1
1
2
·
→
≤
2
·
25
1.3 sec.
G2
1
2
·
→
≤
3
·
156
8 min.
G3
3
3
·
→
≤
2
·
→
≤
2
·
896
3 min.
(1) Number of key variables, (2) number of milestones, and (3) Maximum lengths.Example 14.
Pseudocode3 shows the input file to specify the testing goal G3 in T
G
S
E
N
S. We can also set the testing goal directly in the GUI interface of T
G
S
E
N
S shown in Figure 9(b). The testing goal G3 specifies the following: (i)
key variables (declared in lines 25–28): three variablesMode_A, Mode_B,  and AVin the specification.
(ii)
The list of milestones (declared in lines 4–19):〈
s
1
,
s
2
,
s
3
〉, where s
1 is a state in which Mode_A=Auto, s
2 is a state in which Mode_A=Off, and s
3 is a state in which Mode_A=Auto.
(iii)
maximum lengths between milestones (declared in lines 22-23):s
1
→
≤
2
s
2 and s
2
→
≤
2
s
3.
When the specification forF
l and the testing goal G3 are given, a transition system of this function is first obtained from the result of test case generation. Then, T
G
S
E
N
S automatically searches desired test sequences satisfying the testing goal from the transition system. Pseudocode 4 shows a part of the generated test sequences.
The resulting transition system forF
l has 1,800 states and 77,700 transitions. From the transition system, T
G
S
E
N
S figured out 28 (resp., 32) sequences from s
1 to s
2 (resp., s
2 to s
3) and thus totally 896 (=28 × 32) test sequences satisfying the testing goal only in 3 minutes.Pseudocode 3:An example testing goal.
(
1)
[
AllTransitionFileName
]
(2)
mode_op2.csv;
(3)
(4)
//
Milestone List
(5)      [
MilestoneList
]
(6)    //
first Milestone
(7)   AC::Mode_A#Auto,
(8)   AC::AV#W3,
(9)
AC::AP#KTY3,
(10)
AC::Mode_B#Auto,
(11)
AC::Mode_Change::BU#
Normal,
(12)
AC::BM#Normal,
(13)
AC::BO#Normal;
(14)
(15)
//
second Milestone
(16)
AC::Mode_A#Off;
(17)
(18)
//
third Milestone
(19)
AC::Mode_A#Auto;
(20)
(21)
//
maximum lengths
between two milestones
(22)
[
StepNumList
]
(23)
2,2;
(24)
(25)
[
SelectVarNameList
]
(26)
AC::Mode_A,
(27)
AC::AV,
(28)
AC::Mode_B;Pseudocode 4:An example output: Test sequences.
[
Trace: 0
]
[
AC::Mode_B#Auto, AC::Mode_A#Auto, AC::AV#W3
]
[
AC::Mode_B#Cont, AC::Mode_A#Auto, AC::AV#W1
]
[
AC::Mode_B#Off, AC::Mode_A#Off, AC::AV#W0
]
[
AC::Mode_B#Off, AC::Mode_A#Auto, AC::AV#W1
]
[
AC::Mode_B#High, AC::Mode_A#Auto, AC::AV#W1
]
[
Trace: 1
]
[
AC::Mode_B#Auto, AC::Mode_A#Auto, AC::AV#W3
]
[
AC::Mode_B#Cont, AC::Mode_A#Auto, AC::AV#W1
]
[
AC::Mode_B#Off, AC::Mode_A#Off, AC::AV#W0
]
[
AC::Mode_B#Off, AC::Mode_A#Auto, AC::AV#W3
]
[
AC::Mode_B#High, AC::Mode_A#Auto, AC::AV#W1
]
[
Trace: 2
]
[
AC::Mode_B#Auto, AC::Mode_A#Auto, AC::AV#W3
]
[
AC::Mode_B#Cont, AC::Mode_A#Auto, AC::AV#W1
]
[
AC::Mode_B#Off, AC::Mode_A#Off, AC::AV#W0
]
[
AC::Mode_B#Off, AC::Mode_A#Auto, AC::AV#W2
]
[
AC::Mode_B#High, AC::Mode_A#Auto, AC::AV#W1
]
⋯


## 6. Related Work

Model-based testing technique has been an attractive research area in software engineering field recently [7–9]. Model-based testing is a technique that derives a desired test case from a model or a specification of a system. As modeling makes it possible to refine or check functionality of target systems, we can expect to obtain correct test cases generated from valid models in earlier phases of development. Thus model-based test generation has been attracting the attention of model-driven software development approaches. Model-based testing has two technical issues: modeling target systems appropriately and generating test cases effectively.As for the modeling, many techniques have been proposed, even if we focus on formal modeling only. Models are described based on contracts, abstract data types, process algebras, labeled transition systems, data flow, and so on. These concepts are implemented using specification languages in tools like  VDM [7],  Z [10],  B [11],  Spec# [12], and  JML [13]. With most modeling languages, a user has to specify the systems' behaviors individually.Test case generations from models have been proposed in several ways. Here, test cases include arguments to execute specific functions, pairs of possible inputs and expected outputs, or event sequences. Test cases are searched by tracing executions of models, selecting random values with filtering, or generating candidates with some algorithms.Here, we describe previous works on model-based testing. Spec Explorer [9] generates test cases by state exploration based on multiple strategies from contract-like specifications Spec# on a Microsoft. NET framework. In TGV [8] by INRIA, as a part of the  CADP (Construction and Analysis of Distributed Processes) package, test graphs are generated from labeled transition systems. Uppaal-Tron [14] generates test sequences for real-time systems using the model checker  UPPAAL, and an industrial case study of Uppaal-Tron targeted an electronic refrigerator controller. T-VEC [15] is a coverage-based test generation tool of Simulink/MathWorks which has been used to identify a fault in the Mars Polar Lander.Some model-based test generators use constraints solving to generate test cases. In [16], a test generator based on autofocus is proposed. Autofocus [17] is a graphical tool for model-based development of distributed systems. By translating a specification into a constraint logic program, this generator can deal with all the possible execution traces of the model. TestEra [18] is a test generation framework for Java programs. By considering pre-/postconditions for executing methods as constraints, TestEra generates test cases with  SAT-solvers. Exhaustive generation is available through certain options.Most previous studies targeted the testing of programs or protocols. Although TGV has case studies for small-sized embedded applications, there are only a few studies on the large-scale embedded network systems targeted in our proposed project. Different from other works, we have proposed the original specification language,SENS, focusing on property-based specifications and the tool T
G
S
E
N
S to automatically generate test cases and sequences focusing on testing goals for embedded network systems.


## 7. Conclusion

In this paper, we have proposed a method to automatically generate test cases and sequences based on the specification of embedded networked systems (ENSs). We first proposed a formal specification languageSENS whose features are (
1
) property-based, (
2
) test-oriented, (
3
) object-oriented, (
4
) modular description, and (
5
) lightweight description of time constraints. By the “property-based” feature such that requirements are property-based constraints holding in the entire ENS, logical properties for the system specification are clear and modifications and reuse of the specifications are easy since a part of specifications less affect the entire specifications. Thus,SENS has an advantage on the efficient description and reuse of specifications for large and complicated ENSs. The “object-oriented” and “modular” feature enablesSENS to structurally describe requirement specifications of ENSs consisting of a number of embedded subsystems/equipment. The “lightweight” feature on description of time constraints leads to readily specify embedded systems sensitive to time requirements. In addition, the “test-oriented” feature is helpful for automatic test generation fromSENS specifications. To the best of our knowledge, there has been no other formal specification language having all the above features for ENSs. UsingSENS, we can efficiently describe the requirements of ENSs.We next proposed the methods for automatic test generation in the toolT
G
S
E
N
S whose features are summarized as follows: (
1
)  T
G
S
E
N
S takes specifications of an ENS written inSENS as its input and automatically generates test cases and test sequences; (
2
)  the test case generation problem is translated into a satisfiability problem, and test cases are generated by iteratively using a SAT solver; (
3
)  the test sequences are also automatically obtained based on a testing goal, that is, key variables, milestone states, and a desired maximum length of test sequences, given by a user. We finally applied T
G
S
E
N
S to generate tests for the real air-conditioning systems, and our tool rapidly succeeded in generating about 900,000 test cases in 30 minutes and extract 28 test sequences in 3 minutes.We expect that usingT
G
S
E
N
S can improve the quality of test cases and thus enhance the quality of ENSs. Previously in industrial fields, test cases have often been designed in a manual way. Such the test design depending on testing engineers’ skills seldom covers all the requirements of the complicated ENSs. On the other hand, T
G
S
E
N
S can automatically and mechanically generate test cases from given formal S
E
N
S specifications. Both the description of formal specifications and the automatic test generation lead to improving the quality of test cases. Actually, we found several undefined and under-specified requirements by describing the SENS specifications for real industrial embedded systems as noted in Section 5.2. In addition, T
G
S
E
N
S can generate test cases with 100% coverage for requirements of the given S
E
N
S specification by an exhaustive search using a SAT-based solver. T
G
S
E
N
S also supports feasible test generation by user-specified test filtering and test sequence generation.The successive work of our project is the improvement of our test generator in order to deal with the composition of subsystems. One of the most important aspects of test generation based on formal specifications and models for industrial systems is “scalability.” To overcome this problem, we plan to tackle a higher-speed and more scalable test generation using parallel computing. We also plan to find a constructive way of generating test suites of the whole system from test suites of subsystems as a future work. We also plan to apply the model checking technique to generate more target-specific test cases and sequences.



---

*Source: 909762-2014-05-11.xml*