Vol. 32 No. 1 Feb Processes) [6] [13] CSP CSP [7] CSP CSP PAT [14] FDR2 [4] [7] SD2CSP SD2CSP SDVerifier SDVerifier SD2CSP : 3. 1 : create (

Size: px

Start display at page:

Download "Vol. 32 No. 1 Feb Processes) [6] [13] CSP CSP [7] CSP CSP PAT [14] FDR2 [4] [7] SD2CSP SD2CSP SDVerifier SDVerifier SD2CSP : 3. 1 : create ("

えみゆきしげ
5 years ago
Views:

1 234 SDVerifier: CSP SDVerifier SDVerifier CSP SDVerifier Sequence diagrams are often used in the modular design of softwares. However, it is difficult to verify UML diagrams automatically. In this work, we develop a verification tool of sequence diagrams named SDVerifier. It converts sequence diagrams to processes in CSP, so that existing model checking tool can verify them. One of the main contributions in this work is that counter examples found in the model checking can be translated back to sequence diagrams for supporting to correct their inconsistency. We implemented the tool and conducted experiments with real world case studies. 1 OMG UML [11] UML SDVerifier: A Tool for Verification of Sequence Diagrams using the Process Algebra CSP. Tomohiro Kaizu, Masato Suzuki,, Japan Advanced Institute of Science and Technology. Yoshinao Isobe,, National Institute of Advanced Industrial Science and Technology.,Vol.32, No.1 (2015),pp [ ] [7] CSP (Communicating Sequential

2 Vol. 32 No. 1 Feb Processes) [6] [13] CSP CSP [7] CSP CSP PAT [14] FDR2 [4] [7] SD2CSP SD2CSP SDVerifier SDVerifier SD2CSP : 3. 1 : create ( ) 3. 2 : HTML5 CSS Web 3. 3 : [7] 3 SDVerifier [7] SD2CSP [7] 1 e login, addt ocart, buy logout User login loggedin logout System addt ocart hascart buy 1

3 236 (a) (b) (c) (d) 1: e 1b User addt ocart ok buy ok 1 addt ocart buy ok 1 1 CSP

4 Vol. 32 No. 1 Feb CSP CSP CSP CSP 1a User login ok loggedin CSP User default 1 = Login OK User loggedin User Login User default ( ) 1 User default 1 User default 1 User CSP 1 System default 1 = Login OK System default User loggedin 1 = Add OK User loggedin User loggedin 2 = Buy OK User loggedin System default 2 = Add OK System hascart System hascart 1 = Buy OK System default User loggedin 3 = Buy Empty User loggedin System default 3 = Buy Empty System default User loggedin 4 = Logout OK User default System default 4 = Logout OK System default Login = call.login.user.system Add = call.addt ocart.user.system Buy = call.buy.user.system Logout = call.logout.user.system OK = call.ok.system.user Empty = call.empty.system.user a P a P CSP call CSP CSP $ 2 $ User loggedin User loggedin = (User loggedin 1 User loggedin 2 User loggedin 3 User loggedin 4 ) ${Login, Add, Buy, Logout}

5 238 User loggedin User loggedin {Login, Add, Buy, Logout} User 1 CSP User loggedin 2 Buy OK User loggedin 3 Buy Empty (User loggedin 2 User loggedin 3 ) Buy OK Empty 2 Buy OK Empty (a P ) (a Q) = F a (P Q) (a P ) (b Q) = F (a P ) (b Q) if a b a b P Q (a P ) (b Q) a b a P b Q = F 2 ( ) User loggedin User loggedin = F (Add OK User loggedin Buy (OK User loggedin Empty User loggedin) Logout OK User default) ${Login, Add, Buy, Logout} $ CSP $( ) $ ((a P ) (b Q))$Z = F (a P $Z) (b Q$Z) if a Z, b Z ((a P ) (b Q))$Z = F (a P $Z) (b Q$Z) if a Z, b Z ((a P ) (b Q))$Z = F (a P $Z) (b Q$Z) if a Z, b Z Z (a P ) (b Q) a P b Q a b (a P ) (b Q) a P b Q a b a $ (a P )$Z = F a P $Z (P $Z)$Z = F P $Z User loggedin User loggedin = F (Add OK User loggedin Buy (OK User loggedin Empty User loggedin)

6 Vol. 32 No. 1 Feb CSP [7] 3 SDVerifier (a) User (b) System 2: 1 CSP Logout OK User default) 2 1 CSP τ $ CSP CSP CSP 2 User System login ok addt ocart ok User loggedin buy logout addt ocart System hascart buy User logout addt ocart logout addt ocart SDVerifier PAT [14] PAT CSP PAT [7] SD2CSP SD2CSP 4 EC SD2CSP SDVerifier SD2CSP

240 3: 2 SD2CSP XMI XMI SD2CSP 2 SDVerifier Dart JavaScript Web HTML5 CSS3 SDVerifier 1 3 URL SDVerifier http://dr.asukaze.net/sdverifier/editor.html 1 http://dr.

7 240 3: 2 SD2CSP XMI XMI SD2CSP 2 SDVerifier Dart JavaScript Web HTML5 CSS3 SDVerifier 1 3 URL SDVerifier demo.cgi?model=cart 3 demo.cgi?model=hotel User[user id1] User[user id2] User User SDVerifier 1

8 Vol. 32 No. 1 Feb ClassName [IdName] ClassName IdName 2, 1 1 User User[user id1] User[user id2] user id1 user id2 user id1 user id2 0, 1, 2... ID user id1 user id2 1 1 ID ID ID ID ID ID Id- Name ID ID MessageName(Parameters) Parameters IdName ID ID ID State- Name(Parameters) Parameters IdName ID [7] ID 3 Hotel cancel(rsv id1) User ID

9 242 Hotel cancelled User ID ID 3 Hotel User[user id2] resered(rsv id2) W aiting[wait id] user id2 ID User ID 1 ID 3 getuserid W aiting cancel(user id2) getuserid ID 3 Hotel reserved(rsv id2) Reservation[rsv id2] reserved(rsv id2) user id2 3 Reservation Reservation[rsv id1] Reservation[rsv id2] 2 Reservation 2 2 SDVerifier 3 Reservation[rsv id1] Reservation[rsv id2] Reservation (0) Reservation (1) Reservation (2) PAT Reservation (x) Reservation[rsv id1] Reservation[rsv id2] Reservation (0) Reservation (1) Reservation (2) Reservation (x) 3 4 Reservation 5 3 Hotel CSP [*] PAT CSP call! SenderClass. ReceiverClass. MessageName. P arameters. SenderId. ReceiverId call? SenderClass. ReceiverClass. MessageName. P arameters. SenderId. ReceiverId!? call_?user.hotel.cancel.b1_.b2_.0 Hotel User cancel b1_ b2_ 0 ID 1 Parameters. CSP 5 call! SenderClass. ReceiverClass

10 Vol. 32 No. 1 Feb Reservation (id_) = ( 2 call_?hotel.reservation.create.0.id_ -> Reservation_i3_i30_(id_) 3 [*] end_ -> Skip); 4 5 Reservation_i3_i30_(id_) = 6 call_?hotel.reservation.reserve.b1_.0.id_ 7 -> Reservation_i31_i4_(id_, b1_); 8 9 Reservation_i31_i4_(id_, a1_) = 10 call_!reservation.hotel.reserved.id_ > Reservation_reserved_(id_, a1_); Reservation_reserved_(id_, a1_) = 14 call_?hotel.reservation.cancel.a1_.0.id_ -> Reservation (id_); System_() = User_default_(0) User_default_(1) 17 User_default_(2) Hotel_default_() Waiting (0) 18 Waiting (1) Waiting (2) Reservation (0) 19 Reservation (1) Reservation (2); 4: Reservation CSP ( 3). MessageName. SenderId. ReceiverId call? SenderClass. ReceiverClass. MessageName. SenderId. ReceiverId CSP 5 a1_ a2_ a3_ a4_ a5_ CSP 1 CSP a1_ rsv id1 a2_ user id1 a3_ wait id a4_ user id2 a5_ rsv id2 1 CSP ID 5 2 cancel 17 ok ID 6 cancel 9 cancelled 31 reserve 39 reserved ID 13 getuserid ID wait id 1 [*] ID b3_ 27 create 1 ID 39 reserved SDVerifier ID

11 244 1 Hotel_default_() = (( 2 call_?user.hotel.cancel.b1_.b2_.0 -> Hotel_i1_(b1_, b2_) 3 ) [*] end_ -> Skip); 4 5 Hotel_i1_(a1_, a2_) = 6 call_!hotel.reservation.cancel.a2_.0.a1_ -> Hotel_i2_(a1_, a2_); 7 8 Hotel_i2_(a1_, a2_) = 9 call_!hotel.user.cancelled.0.a2_ -> Hotel_i4_(a1_, a2_); Hotel_i4_(a1_, a2_) = Hotel_i4 sub_1_(a1_, a2_); 12 Hotel_i4 sub_1_(a1_, a2_) = ( 13 [*] b3_:{0..2}@ call_!hotel.waiting.getuserid.0.b3_ 14 -> Hotel_i6_(a1_, a2_, b3_)); Hotel_i6_(a1_, a2_, a3_) = 17 call_?waiting.hotel.ok.b4_.a3_ > Hotel_i7_(a1_, a2_, a3_, b4_); Hotel_i7_(a1_, a2_, a3_, a4_) = 21 call_!hotel.waiting.cancel.a4_.0.a3_ 22 -> Hotel_i8_(a1_, a2_, a3_, a4_); Hotel_i8_(a1_, a2_, a3_, a4_) = 25 Hotel_i8 sub_1_(a1_, a2_, a3_, a4_); 26 Hotel_i8 sub_1_(a1_, a2_, a3_, a4_) = ( 27 [*] b5_:{0..2}@ call_!hotel.reservation.create.0.b5_ 28 -> Hotel_i9_(a1_, a2_, a3_, a4_, b5_)); Hotel_i9_(a1_, a2_, a3_, a4_, a5_) = 31 call_!hotel.reservation.reserve.a4_.0.a5_ 32 -> Hotel_i12_(a1_, a2_, a3_, a4_, a5_); Hotel_i12_(a1_, a2_, a3_, a4_, a5_) = 35 call_?reservation.hotel.reserved.a5_ > Hotel_i13_(a1_, a2_, a3_, a4_, a5_); Hotel_i13_(a1_, a2_, a3_, a4_, a5_) = 39 call_!hotel.user.reserved.a5_.0.a4_ -> Hotel_default_(); 5: Hotel CSP ID SDVerifier 3. 2 SDVerifier create ( ) SDVerifier CSP create create 4 3 Reservation CSP 1 Reservation 2 create

12 Vol. 32 No. 1 Feb cancel 3 Reservation W aiting PAT User Reservation W aiting SDVerifier End states W aiting waiting End states End states End states W aiting waiting waiting End states End states SDVerifier P end SKIP P 5 Hotel default End states 3 [*] end_ -> Skip End states 4 3 [*] end_ -> Skip End states end end SKIP PAT 3. 3 SDVerifier 6 SDVerifier UML XMI XMI UML 3. 4 CSP

246 6: SDVerifier 1b ( 7 ) SDVerifier 7 User @loggedin User loggedin User loggedin User ->

13 246 6: SDVerifier 1b ( 7 ) SDVerifier 7 User loggedin User loggedin User -> System addtocart User System addt ocart { User <- System ok System User ok } [7] SD2CSP XMI [12] XMI

14 Vol. 32 No. 1 Feb User System User -> System addtocart { User <- System ok } User -> System buy { User <- System ok } 7: SDVerifier XMI XMI SD2CSP UML SDVerifier XMI XMI SDVerifier UML XMI UML 3. 4 PAT SDVerifier CSP 6 1 SDVerifier ok User loggedin buy logout addt ocart System hascart buy SDVerifier CSP ID ID state available messages

248 8: 4 SDVerifier [8] EC 4 8 12 8 ServerC

15 248 8: 4 SDVerifier [8] EC ServerC ServerR ServerC ServerR SDVerifier PAT

16 Vol. 32 No. 1 Feb : ( 2.8 GHz Intel Core i7-2640m CPU 8.0 GB RAM) CSP s s s s s s s 3 CSP CSP 2 PAT (AbstractModel \ X) = F (ConcreteModel \ X) AbstractModel CSP ConcreteModel CSP X 2 SDVerifier 8 ServerW refunding refund 2 1 SDVerifier CSP 3 SDVerifier 100 PAT ServerW i7 refunding

17 250 <init -> [int_choice] -> call_.user.serverf.request.0.0 -> [int_choice] -> call_.serverf.serverr.createsubmit.0.0 -> call_.user.serverf.request.1.0 -> call_.serverf.serverr.createsubmit.0.1 -> call_.serverr.serverc.create.0.0 -> call_.serverc.serverr.ok.0.0 -> call_.serverr.serverw.submit > call_.serverr.serverc.create.1.1 -> call_.serverc.serverr.ok.1.1 -> [int_choice] -> call_.serverw.serverr.refund.0.0 -> call_.serverr.servero.refund.0.0 -> call_.serverr.serverc.close.0.0> 9: PAT ServerC[0] closed refunding 1 ServerW ServerC ServerC[0] closed ServerR ServerC close ServerW ServerR refund ServerW ServerR refund ServerW ServerC refunding CSP 2 CSP 5 UML I. Abdelhalim UML fuml CSP [1] L. Dan UML CSP [3] UML 2 alt loop break opt CSP CSP E. Mäkinen MAS [10]

18 Vol. 32 No. 1 Feb Live Sequence Chart HMSC Live Sequence Chart D. Harel [5]. Live Sequence Chart R. Kumar Live Sequence Chart [9] HMSC R. Alur [2] HMSC LTSA Message Sequence Chart plugin (LTSA-MSC) HMSC [15] UML 6 SDVerifier CSP PAT PAT [ 1 ] Abdelhalim, I., Schneider, S. and Treharne, H.: Towards a practical approach to check UML/fUML models consistency using CSP, in Proceeding ICFEM 11 Proceedings of the 13th international conference on Formal methods and software engineering, 2011, pp [ 2 ] Alur, R. and Yannakakis, M.: Model Checking of Message Sequence Charts, in Proceedings of the 10th International Conference on Concurrency Theory, [ 3 ] Dan, L. and Danning, L.: An Approach to Formalize UML Sequence Diagrams in CSP, in 3rd International Conference on Computer and Electrical Engineering, [ 4 ] Formal Systems: FDR2, 2010, com/software.html. [ 5 ] Harel, D. and Kugler, H.: Synthesizing statebased object systems from LSC specifications, in International Journal of Foundations of Computer Science, [ 6 ] Hoare, C. A. R.: Communicating Sequential Processes, Prentice Hall, [ 7 ] Kaizu, T., Isobe, Y. and Suzuki, M.: Refinement and Verification of Sequence Diagrams Using the Process Algebra CSP, IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, Vol. E96-A, No. 2 (2013), pp [ 8 ] Kaizu, T., Isobe, Y. and Suzuki, M.: Verifying sequence diagrams using the process algebra CSP, in AVOCS 2013 Automated Verification of Critical Systems Pre-proceedings, 2013, pp proc kaizu pdf. [ 9 ] Kumar, R. and Mercer, E. G.: Verifying Communication Protocols Using Live Sequence Chart

252 Specifications, in Proceedings of the 8th International Workshop on Automated Verification of Critical Systems, 2008. [10] Mäkinen, E. and Systä, T.

[11] Object Management Group: UML 2.4.1, 2011, http://www.omg.org/spec/uml/2.4.1/. [12] Object Management Group: XMI 2.4.1, 2013, http://www.omg.org/spec/xmi/2.4.1/. [13] Roscoe, A. W.

19 252 Specifications, in Proceedings of the 8th International Workshop on Automated Verification of Critical Systems, [10] Mäkinen, E. and Systä, T.: MAS an interactive synthesizer to support behavioral modelling in UML, in Proceedings of the 23rd International Conference on Software Engineering, [11] Object Management Group: UML 2.4.1, 2011, [12] Object Management Group: XMI 2.4.1, 2013, [13] Roscoe, A. W.: The Theory and Practice of Concurrency, Prentice Hall, [14] Sun, J., Liu, Y. and Dong, J. S.: Model checking CSP revisited: Introducing a process analysis toolkit, Leveraging Applications of Formal Methods, Verification and Validation, Springer, 2009, pp [15] Uchitel, S., Chatley, R., Kramer, J. and Magee, J.: LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios, in Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (2001 ) 2001 ( ) ( ) CSP 1992 ( ) ( ) 2004 / UML

Web Web Web Web i

28 Research of password manager using pattern lock and user certificate 1170369 2017 2 28 Web Web Web Web i Abstract Research of password manager using pattern lock and user certificate Takuya Mimoto In