A framework for modeling and modular verification of component - Based system designs

y T to make it
closed
8 end
9 con f orm = VC(OTi,C, n)
10 if con f orm = true then
11 create LTS Mi from OTi
12 return Mi
13 else
14 v′ = minimum suffix(conform)
that is not in W
15 Add v′ to Mi of OTi
16 end
17 end
18 end
and perform reduction steps (from line 4 to
line 20). When the algorithm halts, if there
is only one CNNFA representation, we can
build the corresponding models for the given
regular expression. Otherwise, the given regular
expression is not valid. The algorithm uses a
stack (line 1) of elements, each of them is either
a symbol from R, or a record Np that stores a
CNNFA representation of the corresponding sub-
regular expression. Detailed information about
the models generation process using CNNFA
algorithm can be found in [19]. The parsing
algorithm is shown in algorithm 7.
5.4. Discussion
From the details of the above algorithms
when generating models, we can see that the
generated models are not optimal. We need
to perform additional tasks to optimize the
generated models. These tasks are converting
C.L. Le et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 2 (2016) 31–42 39
Algorithm 7: Generate models using
CNNFA algorithm
1: Initialize the stack to empty.
2: for each input symbol c in a left-to-right scan
through R do
3: Push c onto the stack.
4: repeat
5: if topmost elements of the stack = λ then
6: Replace by CNNFA representation of λ.
7: else if topmost elements of the stack = a, an
alphabet symbol then
8: Replace by CNNFA representation of a.
9: else if topmost elements of the stack =
NJ |NK then
10: Replace by CNNFA representation of
NJ|K .
11: else if topmost elements of the stack =
NJNK then
12: Replace by CNNFA representation of
NJK .
13: else if topmost elements of the stack = N∗
J
then
14: Replace by CNNFA representation of
NJ∗ .
15: else if topmost elements of the stack = (NJ)
then
16: Replace by NJ .
17: else
18: break;
19: end if
20: until the above steps can no longer be applied
21: end for
models from NFAs to DFAs, then minimizing
the returned DFAs to have the optimal models
using Hopcroft algorithm [2]. You can also
notice that the result models are not LTSs while
the required inputs of the assumption generation
process are LTSs. We notice that if the state
of the component is accepting state every time
an action is performed, then all states of the
generated models are accepting states. Therefore,
those models are LTSs. We can use them in
the assumption generation process. Another
important point here is that in [17], the generation
process is limited by a MaxLength represent for
the longest testable trace against the component
under checking. Generally, using Thompson
algorithm [1] to parse regular expressions to
generate the corresponding models is not limited
by any MaxLength. Therefore, in Table 3,
we don’t have any MaxLength information for
the model generation method using Thompson
algorithm.
6. Assume-Guarantee Verification of
Component-Based Software
Let M1,M2, ...,Mn be models of the system
under checking. These models are generated
from Section 5. We need to verify whether the
system satisfy a predefined safety property p or
not. In this paper, we use assume-guarantee
reasoning approach proposed in [11, 14] to do
this (e.g., to check the formula M |= p, where
M = M1‖M2‖...‖Mn).
For this purpose, the models are divided
into two classes (e.g., fixed and extensional
components). Let M1,M2, ...,Mi be fixed
components and Mi+1, ...,Mn(0 < i < n) be
extensional components, M f = M1‖M2‖...‖Mi
and Me = Mi+1‖...‖Mn are compositional
models of the fixed and extensional components,
respectively. These compositional models and
the property p are inputs of the assume-guarantee
verification method in order to check the system.
The goal of the assume-guarantee verification
method is to verify whether the system satisfies
the property p without composing M f with Me.
For this purpose, an assumption A(p) is generated
by applying the L* learning algorithm [4, 6] such
that A(p) is strong enough for M f to satisfy
p but weak enough to be discharged by Me
(i.e., 〈A(p)〉 M f 〈p〉 and 〈true〉 Me 〈A(p)〉 both
hold, called assume-guarantee rules) [11, 14].
From these assume-guarantee rules, this system
satisfies p without verifying on the whole system.
In order to obtain such appropriate assumptions,
this method applies the assume-guarantee rules
in an iterative process presented in Figure 6. At
each iteration i, a candidate assumption Ai is
produced based on some knowledge about the
system under checking and the results of the
previous iterations. The following two steps
of the assume-guarantee rules are then applied.
Step 1 checks whether M f satisfies p in an
40 C.L. Le et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 2 (2016) 31–42
Fig. 6: Framework for the L*-based assumption generation.
environment that guarantees Ai by computing the
formula 〈Ai〉 M f 〈p〉. If the result is f alse, it
means that this candidate assumption is too weak
for M f to satisfy p. The candidate assumption
Ai therefore must be strengthened with the help
of the produced counterexample cex. Otherwise,
the result is true. In this case, Ai is strong enough
for the property to be satisfied. Then the step 2
is applied for checking whether the component
Me satisfies Ai by computing the formula 〈true〉
Me 〈Ai〉. If this step returns true, the property p
holds in the compositional system M f ‖Me and the
algorithm terminates. Otherwise, this step returns
f alse. In this case, a further analysis is required
to identify whether p is indeed violated in the
system M f ‖Me or the candidate Ai is too strong
to be satisfied by Me. Such analysis is based
on the produced counterexample cex. For the
purpose, the L* algorithm must check whether
the counterexample cex belongs to the unknown
language U = L(AW), where AW is the weakest
assumption which restricts the environment of
M f no more and no less than necessary for p to be
satisfied [10]. If it does not, the property p does
not hold in the system M f ‖Me. Otherwise, Ai is
too strong for Me to satisfy. The consequence
of this is the candidate assumption Ai must be
weakened (i.e., behaviors must be added with the
help of cex) in the next iteration i + 1. A new
candidate assumption may of course be too weak,
and therefore the entire process must be repeated.
7. Experimental Results
In order to show the correctness and feasibility
of the proposed framework, we implemented
tools to support it. We have tested the method
for several systems [8] that contain typical
fragments in sequence diagrams until generating
the corresponding assumptions. The regular
expression generation time is shown in Table 1.
Table 1: Regular expression generation time
No. System Time (ms)
1 Mod channel M1 2.0
2 Mod channel M2 2.0
3 Mod1 M1 4.0
4 Mod1 M2 40.0
5 Mod2 M1 5.0
6 Mod2 M2 4.0
7 Read Write M1 2.0
8 Read Write M2 2.0
9 Simple channel M1 1.0
10 Simple channel M2 2.0
11 Two channel M1 1.0
12 Two channel M2 2.0
13 GasOverControler 9.0
We then test the model generation process
by using the three algorithms of L∗, Thompson,
CNNFA. The generation time is presented in the
table 2. The size of generated models is shown
in the column |M|. The columns |δ| shows the
number of transitions in generated models. The
generated time (in milliseconds) is shown in the
column Time(ms). The maxlength in case of
generating models using L∗ methods is shown in
the column MLen. “Out” in the columns Time
means “Out of memory”, this is the case we could
not generate the model using the corresponding
algorithm.
From Table 2, we have the following
observations:
• Using these testing systems, generating
models using Thompson algorithm is faster
than the other two methods using L∗ and
CNNFA algorithm.
C.L. Le et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 2 (2016) 31–42 41
Table 2: Model generation time
No. Test data
L∗ Thompson CNNFA
|M| |δ| MLen Time |M| |δ| Time |M| |δ| Time
1 Mod channel M1 4 3 3 01.44 3 3 00.17 3 3 00.39
2 Mod channel M2 5 5 4 20.29 3 4 00.26 3 4 11.68
3 Mod1 M1 6 6 3 16.09 5 6 00.75 5 6 26.61
4 Mod1 M2 7 8 4 53.00 5 7 00.83 5 7 233.51
5 Mod2 M1 6 6 3 15.81 5 6 00.75 5 6 76.79
6 Mod2 M2 7 9 4 48.41 5 8 01.02 5 8 421.91
7 Read Write M1 4 3 3 11.63 3 3 00.24 3 3 00.59
8 Read Write M2 4 3 3 14.55 3 3 00.20 3 3 00.74
9 Simple channel M1 4 3 3 11.06 3 3 00.22 3 3 01.73
10 Simple channel M2 4 3 3 15.05 3 3 00.20 3 3 00.74
11 Two channel M1 6 6 3 16.06 5 6 00.80 5 6 25.59
12 Two channel M2 6 6 3 18.55 5 6 00.76 5 6 27.66
13 GasOverControler - - 9 Out 6 10 66.28 7 14 4,668.43
Table 3: Assumption Generation Result
No. System Verification result Time (ms)
1 Read Write acquireRead.acquireWrite 05.50
2 Mod1 OK 13.58
3 Mod2 OK 05.68
4 Mod channel in.send.send.in 00.54
5 Simple channel OK 09.21
6 Two channel OK 02.26
7 GasOverControler OK 13.11
• With the big system (GasOverControler),
using L∗ algorithm cannot generate the
models of the system due to out of memory.
• Using the L∗ algorithm to generate the model
of system is limited by the maxlength of the
traces recognized by the models.
The time of the assumption generation process
is shown in Table 3.
8. Conclusion
We have presented a framework for automated
design verification for component-based
software. The method generates regular
expressions from one of the outputs of the
design phase (sequence diagrams). Models
corresponding to these regular expressions
are then generated. These models are used
to verify whether the design satisfies the
predefined property or not. The whole process
can be re-executed when the design is changed.
Experimental result shows that this method is
feasible with the time of the verification process.
Although the proposed framework can help us
to automatically verify system designs in the form
of sequence diagrams, it still contains several
issues. The first issue is that it is still slow when
testing with large systems. The second is that the
models generated and used during verification is
in the form of LTSs. This is only one kind of
model specification. Currently, the framework
is not for other kinds. Last but not least, the
framework is only applied for safety properties.
What about liveness and fairness ones. Besides,
the framework can be extended to generate test
42 C.L. Le et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 2 (2016) 31–42
paths, test cases and help testing automatically. It
can be very helpful for such organizations that not
have much testing resources.
We are finding a way to apply the method to
some practical and larger systems to prove its
effectiveness. We are also extending the method
using other kinds of output of design phase (e.g.,
class diagrams, state-chart diagrams, etc.) so that
the given system can be verified in all aspects of
design automatically.
Acknowledgments
This work is supported by the project
no. QG.16.31 granted by Vietnam National
University, Hanoi (VNU).
References
[1] K. Thompson, “Regular expression search
algorithm”, Communications of the ACM 11:6
(1968) 419-422.
[2] J. E. Hopcroft, “An nlogn algorithm for
minimizing states in a finite automaton”, Tech.
Report, Stanford University, Stanford, CA, USA,
1971.
[3] T. S. Chow, “Testing software design modeled by
finite-state machines”, IEEE Transactions on Soft.
Engineering, vol. 4(3), pp. 178–187, 1978.
[4] D. Angluin, “Learning regular sets from
queries and counterexamples”, Information
and Computation, vol. 75, no. 2, pp. 87-106,
Nov. 1987.
[5] C. Chang, “From regular expressions to DFA’s
using compressed NFA’s”, Ph.D. Thesis, New
York University, New York, 1992.
[6] R. L. Rivest and R. E. Schapire, “Inference
of finite automata using homing sequences”,
Information and Computation, vol. 103, no. 2,
pp. 299-347, April 1993.
[7] C. Chang, R. Paige, “From regular expressions
to DFA’s using compressed NFA’s”, Theoretical
Computer Science 178, pp. 1-36, 1997.
[8] J. Magee and J. Kramer, Concurrency: “State
Models & Java Programs”, John Wiley & Sons,
1999. The MIT Press, 1999.
[9] J.C. Corbett, M.B. Dwyer, J. Hatcliff, S.
Laubach, C.S. Pasareanu, Robby and Hongjun
Zheng, “Bandera: extracting finite-state models
from Java source code”, Proceedings of the
2000 International Conference on Software
Engineering, pp. 439-448d, 2000.
[10] D. Giannakopoulou, C. Pasareanu, and
H. Barringer, “Assumption generation for
software component verification”, Proc. 17th
IEEE Int. Conf. on Automated Softw. Eng.,
pp. 3–12, Edinburgh, UK, Sept. 2002.
[11] J. M. Cobleigh, D. Giannakopoulou,
C. S. Pasareanu, “Learning Assumptions
for Compositional Verification”, Proc. 9th
International Conference on Tools and Algorithms
for the Construction and Analysis of Systems
(TACAS), pp. 331–346, 2003.
[12] Giannakopoulou, Dimitra and Pasareanu, Corina
S. and Cobleigh, Jamieson M., “Assume-
Guarantee Verification of Source Code with
Design-Level Assumptions”, IEEE Computer
Society, Proceedings of the 26th International
Conference on Software Engineering, pp. 211-
220, 2004.
[13] D. Lorenzoli, L. Mariani and M. Pezze`,
“Automatic generation of software behavioral
models”, ACM, Proceedings of the 30th
international conference on Soft. engineering, pp.
501-510, 2008.
[14] P. N. Hung, T. Aoki and T. Katayama, “Modular
Conformance Testing and Assume-Guarantee
Verification for Evolving Component-Based
Software. IEICE Trans. on Fundamentals”,
Special Issue on Theory of Concurrent Systems
and Its Applications, Vol. E92-A, No.11,
pp. 2772-2780, 2009.
[15] Egyed, A., “Automatically Detecting and
Tracking Inconsistencies in Software Design
Models”, Software Engineering, IEEE
Transactions on , vol.37, no.2, pp.188-204,
March-April 2011.
[16] Zhang Chen, Duan Zhenhua, “Specification
and Verification of UML2.0 Sequence Diagrams
using Event Deterministic Finite Automata”,
pp.41-46, IEEE Computer SocietyWashington,
DC, USA 2011.
[17] L. B. Cuong and P. N. Hung, “A Method for
Generating Models of Black-box Components”,
4th International Conference on Knowledge and
Systems Engineering, IEEE Computer Society
Press, pp. 177-222, 2012.
[18] H.M. Duong, L.K. Trinh and P. N. Hung,
“An Assume-Guarantee Model Checker for
Component-Based Systems”, The 10th IEEE-
RIVF International Conference on Computing
and Communication Technologies, pp. 22–26,
IEEE Computer Society Press, 2013.
[19] Tran, Hoang-Viet and Le, Chi-Luan and Nguyen,
Quang-Trung and Ngoc Hung, Pham, “An
Efficient Method for Automated Generating
Models of Component-Based Software”,
Knowledge and Systems Engineering, Springer
International Publishing, volumn 326, pp. 499-
511, 2015.