5HVRXUFH$QDO\VLVDQG$XWRPDWHG9HULILFDWLRQIRU WKH7KLUW\0HWHU7HOHVFRSHXVLQJ ([HFXWDEOH6\V0/0RGHOV (Invited Talk) 1HULMXV-DQNHYLFLXV 1R0DJLF(XURSH .DXQDV/LWKXDQLD QHULMXV#QRPDJLFFRP Abstract² 6\V0/ DQG LWV VXSSRUWLQJ PRGHOLQJ WRROV KDYH &67 XVHV I80/ DV D IRXQGDWLRQ WR SOXJ LQ DGGLWLRQDO HYROYHG WR VXSSRUW D SUHFLVH H[HFXWLRQ VHPDQWLFV IRU DQ VWDQGDUG HQJLQHV VXFK DV :& 6&;0/ 6WDWH &KDUW ;0/  DXWRPDWHGYHULILFDWLRQRIGHVLJQ PRGHOV7KLVSDSHUJLYHV HQJLQH IRU VWDWH PDFKLQHV >@ -65 IRU VFULSWLQJDFWLRQ DQ RYHUYLHZ RI WKH DSSOLFDWLRQ RI VXFK DQDO\VHV LQ WKH ODQJXDJHV DQG D SDUDPHWULF VROYHU EDVHG RQ 36&6 3UHFLVH FRQWH[W RI WKH 7KLUW\ 0HWHU 7HOHVFRSH 707  RQH RI WKH 6HPDQWLFVRI80/&RPSRVLWH6WUXFWXUHV >@ QH[WJHQHUDWLRQJLDQWRSWLFDOJURXQGEDVHGWHOHVFRSHV 7KH UHVRXUFH DQDO\VLV PDNHV SDUWLFXODU XVH RI WKH SDUDPHWULF VROYHU DQG WKH EHKDYLRU I80/ DQG 6&;0/  Keywords—SysML; Simulation; Model Execution; Verification H[HFXWLRQHQJLQHVRI&67 and Validation; Requirements Verification; Automation; System Requirements; Roll-Up; Test Cases; Analysis; MBSE 7KH SDUDPHWULF VROYHU XVHV WKH I80/ VWDQGDUG WR FUHDWH REMHFWV RI EORFNV 80/ FODVVHV VWHUHRW\SHG ZLWK 6\V0/ %ORFN  DQG VHW WKHLU DWWULEXWH SURSHUW\  YDOXHV $OVR DV , ,1752'8&7,21 6\V0/¶V SDUDPHWULF GLDJUDP LV EDVHG RQ 80/¶V FRPSRVLWH 7KLUW\ 0HWHU7HOHVFRSH 707 >@LV XQGHUGHYHORSPHQW VWUXFWXUHGLDJUDPSRUWV SURSHUWLHVDWWKHERXQGDU\RIFODVVHV  E\WKH707,QWHUQDWLRQDO2EVHUYDWRU\ 7,2 7KHH[DPSOHVLQ DQG FRQQHFWRUV EHWZHHQ SURSHUWLHV  DUH SDUW RI WKH H[HFXWLRQ WKLVSDSHUDUHH[WUDFWHGIURPDSURGXFWLRQOHYHO6\V0/ PRGHO PRGHO ZKLFK LQYROYHV WKH PRGHOLQJ DQG DQDO\VLV RI WKH $OLJQPHQW 2QHQRWDEOHNLQGRIFRQQHFWRULVDELQGLQJFRQQHFWRUZKLFK DQG 3KDVLQJ 6\VWHP $36  IRU WKH 707 GHYHORSHG E\ -HW PDNHV WKH YDOXHV RI SURSHUWLHV DW ERWK HQGV RI WKH FRQQHFWRU 3URSXOVLRQ /DE -3/ ZLWK WKH KHOS RI WKH WRROV SDWWHUQV DQG HTXDO ,I RQH YDOXH FKDQJHV WKH FKDQJH SURSDJDWHV WR WKH PHWKRGV GHYHORSHGE\ 1R 0DJLF ,QF 7KH $36WHDP SXUVXHV RSSRVLWH HQG  7KHVH VHPDQWLFV DOORZ WKH ³JLYHQ´ YDOXHV RI DQ 0%6( DSSURDFK WR DQDO\]H WKH UHTXLUHPHQWV DQG WR SUHERXQG DWWULEXWHV  WR LPPHGLDWHO\ SURSDJDWH DIWHU I80/ GHPRQVWUDWHWKDWWKHVSHFLILHGGHVLJQVDWLVILHVWKHUHTXLUHPHQWV REMHFWLQVWDQWLDWLRQDQGXSGDWHDQ\³WDUJHW´YDOXHV RIXQERXQG %DVHGRQWKHFXVWRPHUVXSSOLHGUHTXLUHPHQWVDQGGHULYHGXVH DWWULEXWHV DIWHUFRQVWUDLQWVHYDOXDWH,QLWLDOO\DWLQVWDQWLDWLRQRI FDVHV WKH JRDOV DUH WR DQDO\]H RSHUDWLRQ VFHQDULRV WR HQVXUH REMHFWVDQGDWWULEXWHV&67DQDO\]HVWKHFDXVDOLW\RIDWWULEXWHV WKDWSRZHUPDVVDQGGXUDWLRQUHTXLUHPHQWVDUHDOZD\VPHWE\ LHGHWHUPLQHVZKLFKDWWULEXWHVDUHJLYHQDQGZKLFKDUHWDUJHW WKHVSHFLILHGV\VWHPGHVLJQ 7KH707PRGHO>@XVHV6\V0/ LQ WKH SDUDPHWULF HTXDWLRQ  ,QLWLDO VROYLQJ SURYLGHV WKH JLYHQ >@DVPRGHOLQJODQJXDJH YDOXHVDQGGHULYHVWKHWDUJHWYDOXHV ,, 67$1'$5'6$1'722/6 :KHQHYHU WKH YDOXH RI DQ DWWULEXWH WKDW LV ERXQG WR FRQVWUDLQWSDUDPHWHUFKDQJHVWKH FRQVWUDLQWLVUHHYDOXDWHGDQG ([HFXWDEOH PRGHOV DUH H[HFXWHG ZLWK WKH KHOS RI DQ XSGDWHV DOO UHODWHG YDULDEOHV FUHDWLQJ D FDVFDGH HIIHFW ZKLFK H[HFXWLRQ RU VLPXODWLRQ HQJLQH 7KH H[HFXWLRQ RI WKH PRGHOV PD\ WULJJHU PRUH DQG PRUH UHODWHG FRQVWUDLQWV HYDOXDWLRQV ,I ZDVSHUIRUPHGXVLQJWKH&DPHR6LPXODWLRQ7RRONLW &67 >@ WKDW KDSSHQV GXULQJ EHKDYLRUV H[HFXWLRQ VWDWH PDFKLQH RU ZKLFKLVDSOXJLQWR0DJLF'UDZ>@HQDEOLQJPRGHOH[HFXWLRQ DFWLYLW\  &67 UHHYDOXDWHV WKH SDUDPHWULFV DQG FRQVLGHUV DQ IRUHDUO\V\VWHPEHKDYLRUVLPXODWLRQ HQWLUHFDVFDGHDVSDUWRIWKHUXQWRFRPSOHWLRQVWHS DQDWRPLF &67 LV D VLPXODWLRQ SODWIRUP EDVHG RQ 20* I80/ DFWLRQ ZKLFK KDSSHQV DW WKH VDPH LQVWDQW RI WLPH  &67 LV VWDQGDUG>@ZKLFKGHILQHVSUHFLVHPRGHOH[HFXWLRQVHPDQWLFV IOH[LEOH LQ GHDOLQJ ZLWK XQGHUVSHFLILHG PRGHOV DV LW ILOOV LQ DQGDYLUWXDOPDFKLQHIRU80/ >@HQDEOLQJFRPSOLDQWPRGHOV DXWRPDWLFDOO\VRPHJDSVFRQFHUQLQJLQLWLDOFRQGLWLRQV HJQRW WR EH WUDQVIRUPHG LQWR YDULRXV H[HFXWDEOH IRUPV IRU DOO SDUDPHWHUV RI DFWLYLWLHV YDOXH SURSHUWLHV QHHG WR EH IXOO\ YHULILFDWLRQ 2 VSHFLILHG  %DVHG RQ WKLV IHDWXUH RI &67 G\QDPLF EHKDYLRU IRUPDOL]HG LQWR VRFDOOHG SURSHUW\EDVHG UHTXLUHPHQWV   EDVHG UROOXSVXVLQJSDUDPHWULFVLVEXLOWLQWKHUXQQLQJPRGHO ZKLFK DOORZ IRU D IRUPDOL]HG WUDFH RI UHTXLUHPHQWV LQWR WKH GHVLJQ 7KH DVVSHFLILHG FRQFHSWXDO GHVLJQ   DQGRU WKH ,,, $8720$7('5(48,5(0(1769(5,),&$7,21$1'6<67(06 UHDOL]DWLRQ GHVLJQ   DUH YHULILHG DJDLQVW WKH FKDQJHG $1$/<6,6 :,7+6<60/ UHTXLUHPHQW UHVXOWLQJ LQ SDVV RU IDLO   7KH V\VWHPV 7KH ([HFXWDEOH 6\VWHP (QJLQHHULQJ 0HWKRG (6(0  >@ PRGHOLQJ HQYLURQPHQW DQG FKDQJH VFHQDULR LV GHVFULEHG LQ GHILQHVVWHSVDQGSDWWHUQVWRFRQVWUXFWDQH[HFXWDEOHPRGHOWR PRUHGHWDLOLQ>@ FDUU\RXWUHVRXUFHDQDO\VLV  )RUPDOL]H5HTXLUHPHQWV 5HTXLUHPHQWVDUHVSHFLILHGE\6\V0/%ORFNVDQG &RQVWUDLQW%ORFNVZKHUHD%RROHDQH[SUHVVLRQGHILQHV WKHUHTXLUHPHQW  6SHFLI\'HVLJQ 7KHV\VWHPGHVLJQLVVSHFLILHGE\GHFRPSRVLWLRQWUHHV RILWVIXQFWLRQDODQGSK\VLFDODVSHFWV  &KDUDFWHUL]H&RPSRQHQWV 7KHLQGLYLGXDOFRPSRQHQWVDUHDXJPHQWHGE\D VWDQGDUGPRGHOLQJSDWWHUQDGGLQJVHYHUDOSURSHUWLHV HJSRZHUPDVVGXUDWLRQ XVHGLQWKHDQDO\VLV  6SHFLI\$QDO\VLV&RQWH[W )LJXUH7LPHOLQHRIFRPSRQHQWVWDWHV 7KH$QDO\VLVFRQWH[WELQGVIRUPDOUHTXLUHPHQWVWRWKH DVGHVLJQHGV\VWHPSURSHUWLHVIRUDQDO\VLV  6SHFLI\2SHUDWLRQDO6FHQDULRV 2SHUDWLRQDOVFHQDULRVHODERUDWHFXVWRPHUXVHFDVHVDV DVHTXHQFHRUDFWLYLW\GLDJUDP2SHUDWLRQDOVFHQDULRV H[HUFLVHGLIIHUHQWFRQILJXUDWLRQHJIRUSRZHU FRQVXPSWLRQ  6SHFLI\&RQILJXUDWLRQV 7KHLQLWLDOVWDWHRIWKHRSHUDWLRQDOVFHQDULRV LQWKLV FDVHHJWKHLQLWLDOSRZHUFRQVXPSWLRQ FRQILJXUDWLRQV LVVSHFLILHGZLWKGLIIHUHQW GHFRPSRVLWLRQWUHHVRILQVWDQFHVSHFLILFDWLRQV  5XQ$QDO\VLV 7KHFRQILJXUHGDQDO\VLVLVUXQ XVLQJDVLPXODWLRQ HQJLQHVXFKDV&677KLVSURYLGHVVHYHUDORXWSXWV VXFKDVD WLPHOLQHRIWKHVWDWHVRIWKHLQGLYLGXDO FRPSRQHQWVZKLFKVKRZVVWDWHFKDQJHVRILQGLYLGXDO FRPSRQHQWVGXULQJWKHVLPXODWLRQ )LJ E UROOHGXS SRZHUDQGPDUJLQDQGF YDOXHSURILOHVZKLFKVKRZ )LJXUH3RZHUSURILOHV RI$36 VXEV\VWHPV WKHWRWDOYDOXHRYHUWLPHRIWKHUROOHGXSYDOXH HJ WRWDOSRZHURIGRPHLQVWDOODWLRQSDUWRIWKH $36 ± VHH )LJ7KHVHSURGXFWVUHSUHVHQWGLIIHUHQWYLHZVWKDW FDQEHXVHGE\WKHHQJLQHHUWRDQDO\]HWKHUHVXOWV $V VRRQ DV WKH UHVXOWV RI WKH GLIIHUHQW VFHQDULRV DUH DYDLODEOHWKHVDWLVIDFWLRQRIWKHRULJLQDOFXVWRPHUUHTXLUHPHQW KDV WR EHGHPRQVWUDWHG7KLV LV GRQH ZLWK D VHSDUDWH DQDO\VLV FRQWH[W $W\SLFDOVFHQDULRWRYHULI\WKHDVGHVLJQHGV\VWHPLVZKHQ DUHTXLUHPHQWFKDQJHV )LJ  $FKDQJH  RID707UHTXLUHPHQW NHSWLQ'2256   DVPDQDJHPHQWWRROIRUWH[WXDOUHTXLUHPHQWV LVSURSDJDWHGWR WKH6\V0/PRGHOPDQDJHGLQDPRGHOUHSRVLWRU\ZKHUHLWLV )LJXUH3URSDJDWLRQRIDFKDQJHLQWKHUHTXLUHPHQWVRI$36 3 ,9 /(66216$1' (;3(5,(1&(*$7+(5(')5207+( 7KHSUHVHQWHGSUDFWLFH LQWHJUDWHVWKHVWDQGDUGSDWWHUQRIDQ (;(&87$%/(707 02'(/ DQDO\VLV FRQWH[W ZLWK WKH EHKDYLRU H[HFXWLRQ SDWWHUQ E\ VSHFLI\LQJDVFHQDULRDVWKHEHKDYLRURIWKHDQDO\VLVFRQWH[W¶V %\GULYLQJWKHDQDO\VLVGLUHFWO\IURPGDWDLQWKHPRGHOWKH FODVVLILHU 7KH LQVWDQFH RI WKH DQDO\VLV FRQWH[W FRQWDLQV WKH LQFRQVLVWHQF\WKDWRIWHQHPHUJHV ZKHQGDWDLVDOVRPDLQWDLQHG FXUUHQWVWDWHRIWKHVFHQDULRDQGWKHSDUDPHWULFVFRPSXWHWKH LQ DQDO\VLV WRROV HJ ([FHO ZDV HOLPLQDWHG ,Q DGGLWLRQ YDOXHV RI VHOHFWHG SURSHUWLHV DV WKH VFHQDULR UXQV 7KH LQLWLDO SHUIRUPLQJ WKH DQDO\VLV E\ VLPXODWLQJ WKH V\VWHP GHVLJQ VWDWH IRU WKH DQDO\VLV FRQWH[W FRPHV IURP D WUHH RI LQVWDQFH FDSWXUHG LQ WKH PRGHO KDV WKH DGGHG EHQHILW RI KDYLQJ DOO WKH VSHFLILFDWLRQV DQG WKHLU SURSHUW\ YDOXHV D FRQILJXUDWLRQ  DQG QHFHVVDU\LQIRUPDWLRQ HJWKHVWDWHRIWKHV\VWHPDWUHOHYDQW WKHRXWSXWLVDQRWKHUWUHHWKDWGLVSOD\VWKHFRPSXWHGYDOXHVRI WLPH SRLQWV  UHDGLO\ DYDLODEOH WR FKHFN 7KLV PDNHV WKH WKHDQDO\VLV GHYHORSPHQW RI DQDO\VLV SDWWHUQV HJ UROOXSV  WR FKHFN WKH VDWLVIDFWLRQRIUHTXLUHPHQWVUHDVRQDEO\VWUDLJKWIRUZDUG 7KHUHDUH SODQV WRLPSURYHVRPHRIWKHSDWWHUQVUHODWHGWR EHKDYLRUPRGHOLQJWRVXSSRUWH[HFXWDELOLW\)RUH[DPSOHWKHUH 'LIIHUHQWUROOXSVFDQEHDSSOLHGWRGLIIHUHQWFKDUDFWHULVWLFV LVDQHHG WRILQGDPRUHIRUPDOZD\WRWLHFRQVWUDLQWVRQYDOXH RI D V\VWHP OLNH SRZHU DQG PDVV 7KH\ DOO IROORZ WKH VDPH SURSHUWLHV IRU HDFK SRZHU PRGH WR WKH VWDWH ,W LVGHVLUDEOH WR EDVLF SDWWHUQ 2ULJLQDOO\ WKH PDVV DQG SRZHU UROOXSV IRU WKH LPSURYH WKH UROOXS SDWWHUQ WKDW GHDOV ZLWK VWDWH VSHFLILF $36ZHUHPDLQWDLQHGDQGFDOFXODWHGLQ([FHOVSUHDGVKHHWVIRU FRQVWUDLQWVE\DYRLGLQJKDUGFRGLQJFRQVWUDLQWYDOXHVLQVWDWH GLIIHUHQW VLPSOLILHG  VFHQDULRV DQG XSGDWHG ZKHQHYHU D LQYDULDQWRURWKHUFRQVWUDLQWV)XUWKHUPRUHUXQQLQJVLPXODWLRQV UHTXLUHPHQW RU WKH V\VWHP GHVLJQ FKDQJHG +RZHYHU LW ZDV JHQHUDWHVDODUJHDPRXQWRIUHVXOWVZKLFKDUHFXUUHQWO\VWRUHG FRPSOHWHO\GLVFRQQHFWHGIURPWKH6\V0/V\VWHPPRGHOZKLFK LQLQVWDQFHVSHFLILFDWLRQVZKLFKPDNHWKHGHVLJQPRGHOJURZ FDSWXUHVWKHGLIIHUHQWRSHUDWLRQDOVFHQDULRVWKHV\VWHPGHVLJQ XQQHFHVVDULO\ 7KRVH UHVXOWV VHTXHQFH GLDJUDP UHFRUGLQJ DQG WKH UHTXLUHPHQWV ,QWHJUDWLQJ WKH UROOXSV VLPSOLILHG WKH LQVWDQFHVQDSVKRWVVLPXODWLRQORJV VKRXOGEHVWRUHGRXWVLGHRI PDLQWHQDQFH DQG FRQVLVWHQF\ RI WKH GDWD FKDQJH ZDV RQO\ LQ WKHV\VWHPPRGHOLQGHGLFDWHGGDWDUHSRVLWRU\ RQH SODFH WKH V\VWHP PRGHO  DQG KHOSHG DXWRPDWH WKH FKHFNLQJRIUHTXLUHPHQWVDWLVIDFWLRQ$QRWKHUDGGHGEHQHILWLV WKDW SHUIRUPLQJ WKH DQDO\VLV RQ WKH V\VWHP PRGHO GLUHFWO\ 9, $&.12:/('*(0(176 DOORZVWKHDQDO\VLVUHVXOWWRVWD\LQWKHPRGHOZKLFKPDNHVWKH 7KH DXWKRU ZRXOG OLNH WR DFNQRZOHGJH WKH PDMRU RQJRLQJ HQJLQHHULQJGRFXPHQWWKDWZRXOGEHJHQHUDWHGIURPWKHPRGHO FRQWULEXWLRQVRI5REHUW.DUEDQWRWKHHYROXWLRQRIV\VWHPOHYHO VWD\XSWRGDWHDQGFRQVLVWHQW EHKDYLRUVSHFLILFDWLRQDQGDQDO\VLVZLWKH[HFXWDEOHPRGHOV 2EYLRXVO\ QRW DOO NLQGV RI V\VWHP DQDO\VLV HJ ILQLWH HOHPHQW DQDO\VLV  FDQ EH SHUIRUPHG XVLQJ WKH VHPDQWLFV RI 5()(5(1&(6 6\V0/DORQH7KHVHDQDO\VHVZRXOGUHTXLUHWKHDXJPHQWDWLRQ >@ 1R0DJLF,QF ³0DJLF'UDZ´ KWWSZZPDJLFGUDZFRP RI 6\V0/ ZLWK RWKHU SURILOHV WKDW FDSWXUH WKH PLVVLQJ >@ 1R0DJLF,QF ³&DPHR6LPXODWLRQ7RRONLW´ LQIRUPDWLRQ $OVR WKH UHOLDELOLW\ RI WKH DQDO\VHV WKDW FDQ EH KWWSZZZQRPDJLFFRPSURGXFWVPDJLFGUDZDGGRQVFDPHRVLPXODWLRQ SHUIRUPHG XVLQJ WKLV PHWKRG UHOLHV RQ WKH UHOLDELOLW\ RI WKH WRRONLWKWPO >@ 20* ³6\VWHPV0RGHOLQJ/DQJXDJH 6\V0/ 9HUVLRQ´ 6\V0/VLPXODWLRQWRROVZKLFK PD\EHOHVVPDWXUHWKDQWKHLU >@ 20*  ³6HPDQWLFV RI D )RXQGDWLRQDO 6XEVHW IRU ([HFXWDEOH 80/ JHQHUDOSXUSRVHFRXQWHUSDUWV +RZHYHUWKLVLVRIWHQPLWLJDWHG 0RGHOV )80/ 9HUVLRQ´ E\LQWHJUDWLQJWKHIRUPHUZLWKWKHODWWHU >@ 20* ³8QLILHG0RGHOLQJ/DQJXDJH 80/ 9HUVLRQ´ >@ 20*  ³3UHFLVH 6HPDQWLFV RI 80/ &RPSRVLWH 6WUXFWXUHV 36&6  9HUVLRQ´ 9 &21&/86,216$1')8785(:25.6 >@ :&  ³6WDWH &KDUW ;0/ 6&;0/  6WDWH 0DFKLQH 1RWDWLRQ IRU 5HTXLUHPHQW YHULILFDWLRQ LV DQ LPSRUWDQW NLQG RI DQDO\VLV &RQWURO$EVWUDFWLRQ:&5HFRPPHQGDWLRQ´ >@ :&³:RUOG:LGH:HE&RQVRUWLXP´ KWWSZZZZRUJ WKDWLVRIWHQSHUIRUPHGLQWKHFRQWH[WRI0%6(,QWKLVSDSHUD >@ .DUEDQ5 -DQNHYLþLXV 1(ODDVDU0³(6(0$XWRPDWHG6\VWHP UXQQLQJ H[DPSOH GHULYHG IURP DQ LQGXVWULDO FDVH VWXG\ ZDV $QDO\VLVXVLQJ([HFXWDEOH6\V0/0RGHOLQJ3DWWHUQV´$QQXDO,1&26( SUHVHQWHG ,Q WKH VDPSOH D SUDFWLFH LV XVHG ZKHUH DXWRPDWHG ,QWHUQDWLRQDO6\PSRVLXP ,6 (GLQEXUJK8. UHTXLUHPHQWV YHULILFDWLRQ ZLWK D VHW RI H[HFXWDEOH 6\V0/ >@707 ³7KLUW\0HWHU7HOHVFRSH´ KWWSZZZWPWRUJ PRGHOLQJ SDWWHUQV LV GHSOR\HG 7KHVH SDWWHUQV LQWHJUDWH >@ .DUEDQ5'HNHQV) -DQNHYLþLXV 1(ODDVDU0 ³&UHDWLQJ6\VWHP (QJLQHHULQJ3URGXFWVZLWK([HFXWDEOH0RGHOVLQD0RGHO%DVHG SDUDPHWULFV ZLWK WKH H[HFXWLRQ VHPDQWLFV RI EHKDYLRUDO (QJLQHHULQJ(QYLURQPHQW´ 0RGHOLQJ6\VWHPV(QJLQHHULQJDQG3URMHFW GLDJUDPV 0DQDJHPHQWIRU$VWURQRP\9, 63,((GLQEXUJK8. >@³707PRGHO´ KWWSVJLWKXEFRP2SHQ0%((7076\V0/0RGHO 4