IPSJ SIG Technical Report Vol.2015-SE-189 No /7/23 iarch-u 1,a) 1,b) 1,c) 1,d) Archface-U iarch-u Partial Model !" %&)*+,-./ :;<

Similar documents
IPSJ SIG Technical Report Vol.2013-HCI-152 No /3/13 1,a) 1,b) 2,c) / GPS Bluetooth(BT) WiFi BT WiFi 1. Bluetooth WiFi 1 / 1 2 a)

VDM-SL ISO.VDM++ VDM-SL VDM- RT VDM++ VDM,.VDM, [5]. VDM VDM++.,,, [7]., VDM++.,., [7] VDM++.,,,,,,,.,,, VDM VDMTools OvertureTo

福岡大学人文論叢47-3

<8CA48B8694EF8E E E816991E C5816A5F8DC58F4994C52E706466>

2 3 Pockets Pockest Java [6] API (Backtracking) 2 [7] [8] [3] i == Pockets 2.1 C3PV web [9] Pockets [10]Pockets 1 3 C

2

main.dvi


. IDE JIVE[1][] Eclipse Java ( 1) Java Platform Debugger Architecture [5] 3. Eclipse GUI JIVE 3.1 Eclipse ( ) 1 JIVE Java [3] IDE c 016 Information Pr

The copyright of this material is retained by the Information Processing Society of Japan (IPSJ). The material has been made available on the website

A Study on Throw Simulation for Baseball Pitching Machine with Rollers and Its Optimization Shinobu SAKAI*5, Yuichiro KITAGAWA, Ryo KANAI and Juhachi

IPSJ SIG Technical Report Vol.2013-CE-122 No.16 Vol.2013-CLE-11 No /12/14 Android 1,a) 1 1 GPS LAN 2 LAN Android,,, Android, HTML5 LAN 1. ICT(I

3.1 Thalmic Lab Myo * Bluetooth PC Myo 8 RMS RMS t RMS(t) i (i = 1, 2,, 8) 8 SVM libsvm *2 ν-svm 1 Myo 2 8 RMS 3.2 Myo (Root

/ , ,908 4,196 2, ,842 38, / / 2 33 /

ses2011-tutorial.pptx

258 5) GPS 1 GPS 6) GPS DP 7) 8) 10) GPS GPS ) GPS Global Positioning System

IPSJ SIG Technical Report Vol.2012-MUS-96 No /8/10 MIDI Modeling Performance Indeterminacies for Polyphonic Midi Score Following and

MDD PBL ET 9) 2) ET ET 2.2 2), 1 2 5) MDD PBL PBL MDD MDD MDD 10) MDD Executable UML 11) Executable UML MDD Executable UML

CX-Checker CX-Checker (1)XPath (2)DOM (3) 3 XPath CX-Checker. MISRA-C 62%(79/127) SQMlint 76%(13/17) XPath CX-Checker 3. CX-Checker 4., MISRA-C CX- Ch

1: A/B/C/D Fig. 1 Modeling Based on Difference in Agitation Method artisoc[7] A D 2017 Information Processing

Vol.55 No (Jan. 2014) saccess 6 saccess 7 saccess 2. [3] p.33 * B (A) (B) (C) (D) (E) (F) *1 [3], [4] Web PDF a m

B HNS 7)8) HNS ( ( ) 7)8) (SOA) HNS HNS 4) HNS ( ) ( ) 1 TV power, channel, volume power true( ON) false( OFF) boolean channel volume int

VHDL-AMS Department of Electrical Engineering, Doshisha University, Tatara, Kyotanabe, Kyoto, Japan TOYOTA Motor Corporation, Susono, Shizuok

IPSJ SIG Technical Report Vol.2010-NL-199 No /11/ treebank ( ) KWIC /MeCab / Morphological and Dependency Structure Annotated Corp

xx/xx Vol. Jxx A No. xx 1 Fig. 1 PAL(Panoramic Annular Lens) PAL(Panoramic Annular Lens) PAL (2) PAL PAL 2 PAL 3 2 PAL 1 PAL 3 PAL PAL 2. 1 PAL

IPSJ SIG Technical Report Vol.2014-DBS-159 No.6 Vol.2014-IFAT-115 No /8/1 1,a) 1 1 1,, 1. ([1]) ([2], [3]) A B 1 ([4]) 1 Graduate School of Info

Convolutional Neural Network A Graduation Thesis of College of Engineering, Chubu University Investigation of feature extraction by Convolution

3_23.dvi

paper.pdf

, : GUI Web Java 2.1 GUI GUI GUI 2 y = x y = x y = x

2. CABAC CABAC CABAC 1 1 CABAC Figure 1 Overview of CABAC 2 DCT 2 0/ /1 CABAC [3] 3. 2 値化部 コンテキスト計算部 2 値算術符号化部 CABAC CABAC


XML Tool to Check the Consistency both Software Documents Using XML and Source Programs 1 Summary. Generally, a software consists of source programs a

Lyra X Y X Y ivis Designer Lyra ivisdesigner Lyra ivisdesigner 2 ( 1 ) ( 2 ) ( 3 ) ( 4 ) ( 5 ) (1) (2) (3) (4) (5) Iv Studio [8] 3 (5) (4) (1) (

Study on Throw Accuracy for Baseball Pitching Machine with Roller (Study of Seam of Ball and Roller) Shinobu SAKAI*5, Juhachi ODA, Kengo KAWATA and Yu

IHI Robust Path Planning against Position Error for UGVs in Rough Terrain Yuki DOI, Yonghoon JI, Yusuke TAMURA(University of Tokyo), Yuki IKEDA, Atsus


6 2. AUTOSAR 2.1 AUTOSAR AUTOSAR ECU OSEK/VDX 3) OSEK/VDX OS AUTOSAR AUTOSAR ECU AUTOSAR 1 AUTOSAR BSW (Basic Software) (Runtime Environment) Applicat

97-00

THE INSTITUTE OF ELECTRONICS, INFORMATION AND COMMUNICATION ENGINEERS TECHNICAL REPORT OF IEICE {s-kasihr, wakamiya,

DesignOfPLEASE0612.ppt

STARTプログラム.indd

1 UD Fig. 1 Concept of UD tourist information system. 1 ()KDDI UD 7) ) UD c 2010 Information Processing S

58.pdf

1. HNS [1] HNS HNS HNS [2] HNS [3] [4] [5] HNS 16ch SNR [6] 1 16ch 1 3 SNR [4] [5] 2. 2 HNS API HNS CS27-HNS [1] (SOA) [7] API Web 2

Transcription:

iarch-u 1,a) 1,b) 1,c) 1,d) Archface-U iarch-u Partial Model 1. 123+!" %&)*+,-./0 46789 :;<=> ( 1) Archface-U [7] Archface-U Archface-U iarch-u 2 Archface-U 3 1 Kyushu University a) fukamachi@posl.ait.kyushu-u.ac.jp b) ubayashi@ait.kyushu-u.ac.jp c) hosoai@qito.kyushu-u.ac.jp d) kamei@ait.kyushu-u.ac.jp!"#$ %& '( 2?@!"#$%&' EFGH (')"#$%&'*+7ABCD, 1 Archface- U Partial Model 4 Archface-U iarch-u 6 2. Archface-U 2.1 Diego (Location) (Level) (Nature) 3 []( 2) Archface-U Diego 2.1.1 1

1 0 1 Archface-U 0 ( ) 3. 2 Diego [] 3 2.1.2 0 4 0 1 2 3 4 2.1.3 2.2 2.1 2 Famelis Partial Model [2] Archface-U [7] 3.1 Partial Model Famelis Partial Model Partial Model Diego Archface-U Partial Model 3 P2P 6 (a-f) Partial Model (g) Partial Model Partial Model OR Partial Model Partial Model Φ M Φ P Φ M Φ P Φ M Φ P SAT SAT 1 2

どれを実装するかが不確か 実装するかどうかが不確か 4 Archface-U 3 P2P 6 (a-f) Partial Model (g)[2] 1 Partial Model M p [2] Φ M Φ P Φ M Φ P Property p SAT SAT Maybe SAT UNSAT True UNSAT SAT False UNSAT UNSAT (error) True False Maybe Φ M Φ P Φ M Φ P SAT Φ M Φ P Φ M Φ P Maybe UNSAT Partial Model error 3.2 Archface-U 3.2.1 Archface-U Archface [6] Archface-U [7] Archface Java Archface Archface Archface iarch Archface Archface-U Archface-U Archface Certain Archface Uncertain Archface 2 ( 4) Uncertain Archface Certain Archface Archface-U Component-and-Connector [1] Archface-U Archface-U 2 (1) (2) 2 1 Alternative 2 Optional Archface-U Java Archface-U 3.2.2 Certain Archface Certain Archface Archface 2 3 P2P 3

1 interface component Node{ 2 void start(); 3 void cancel(); 4 void completed(); } 6 uncertain component unode extends Node{ 7 [void restart();] 8 { 9 void share(), 10 void share(file file) 11 }; 12 } 13 14 interface connector cp2psystem{ 1 Node = (Node.start -> Node.cancel -> Node); 16 } 17 uncertain connector ucp2psystem 18 extends cp2psystem{ 19 Node = (Node.start -> Node.completed 20 -> [Node.restart] -> Node.cancel -> Node); 21 } P2P Archface-U interface component Java Java start interface connector FSP Finite State Process [4] Node.start Node.cancel Node 3.2.3 Uncertain Archface Uncertain Archface Optional Alternative 2 2 Optional [] Alternative {} Uncertain Archface Uncertain Archface Uncertain Archface Certain Archface!"#$%&'-./012!"#$%&'()*+,!"#$%&#'()9:;<=>?@ *&"+,&-./01'-9:;<=>?@ AB 34 6 7,8 6 Uncertain Archface Java 1 Uncertain Archface uncertain connector Node restart Optional start -> completed -> restart -> cancel start -> completed -> cancel 2 3 (a) (b) Partial Model Archface-U [7] Partial Model Archface-U 3.3 ( 6) Partial Model Partial Model 3.1 3.1 [2] Partial Model Archface-U Partial Model Archface-U Archface-U 3.2 4

()*+,-./!"#$%&#'()01234,678 9:2%7./!"#$ 7 ;<=>?@AB"%%*+ ;<=>?@AB CD%&'*+EF!" #$ %&' iarch-u Archface-U 3.2 Optional Alternative 4. iarch-u Archface iarch iarch-u iarch-u Archface-U LTSA (Labelled Transition System Analyser) [4] ( 4) 4.1 Archface-U Archface-U Eclipse Archface-U Archface-U Java Archface-U 3.2 Java Archface-U Eclipse XText API AST(Abstract Syntax Tree) ( 8) 4.2 [3] Archface-U JUnit AspectJ AspectJ Weaving 4.3 LTSA LTSA Magee [4] LTSA LTS Labelled Transition System FSP 3.2 Archface-U FSP Optional Alternative LTSA LTSA Archface-U. 3 P2P.1.1.1 P2P 3 (a) (b) (a) (b) Seeding restart DevOps ( ) DevOps (a) (b)

情報処理学会研究報告!"#$%&#'()!"#"!"# *+,!$%&'()" 図 8 Archface-U コンパイラ エディタ もあり得る.1.2 我々の開発プロセスによる不確かさへの対処 不確かさの表現: まず 設計段階で発生した restart を *+,#$%&'(&)!"#$%&#'() 行うかどうか という Optional な不確かさを表すことを 考える 我々のアプローチでは この Optional な不確か!"#! さを 設計段階では Partial Model を使って表すことがで!" きる 3.1 節にも示したとおり Partial Model を作成する ことで このフロー自体のプロパティ *1 について検査を行 うことができ 顧客が提示する不確かな要求がフローの前 提条件を崩さないかを確認することができる 次に 不確かさを包容しつつも安全性が確認できた設計 モデルを 実装に落としこむことを考える このとき 本 開発プロセスでは Partial Model を Archface-U へ変換す る Archface-U へ変換することで Partial Model で表現 された不確かさを引き継いだまま実装へつなげることがで きる Archface-U は単なるドキュメントとして不確かさを 実装へ引き継ぐだけではなく 3.2 節でも述べたように Archface-U は実装に対して型検査を行う 型検査をこの 例に用いた場合 現在 モデル (a) (b) のいずれに従って 実装を行っているかを確認することが可能となる (図 9) これは 4.1 節で述べたコンパイラによるメッセージによっ て確認をすることができる また モデル (a) (b) のいず れにも従っていない実装を行っている場合 その結果がコ *1 例えば 今回の例では どの状態においても Idle 状態へ戻るこ とができる などが考えられる 201 Information Processing Society of Japan 図 9 Archface-U の型検査による実装が従っているモデルの判別 ンパイルエラーとして表示される そのため 不確かさを 抱えている場合でも設計に従った実装を行うことが可能と なる 不確かさの解決: 不確かさが実装段階で解決される場合を 考える 今回の例では 実装段階で顧客がモデル (a) の設 計でシステムを作って欲しいと要求が確定したとする こ のことで 不確かさが解決したため Archface-U の記述 を変更することで 不確かさが解決したことを表す 具 体的には Archface-U において restart の記述を削除 するだけでよい 逆に 顧客がモデル (b) を望んだ場合は restart の [ ] を外すことによって確定することができる.2 不確かさが実装段階で発生 実装段階で解決 この節では 実装段階で不確かさが発生し 実装段階で 6

!" #$ %&'()#$*+, %&'()#$*-.!"#$%&'!"#$%&()*%+,)*%' Archface-U (1) Archface-U (2) Archface-U 10 Archface-U VCS.2.1 P2P share share share share File.2.2 : Archface-U share Alternative Archface-U Archface-U Git VCS( : Version Controll System) Archface-U share share VCS ( 10) : 2 (1) (2).3.3.1 P2P share share share share bigdatashare bigdatashare share 2.3.2 : Archface-U share bigdatashare Alternative share bigdatashare 2 : Archface-U AOP (Aspect Oriented Programming) 4.2 Weaving AspectJ ( 11) share 7

!"#$%!"#$%"!"#$$ %&$%'()&* +,&$% -(.)/%&$%01#2&34*!"#$"%&' (!)#$*%&' ( 11!"#$" ()*+,-. &"*+,-./0&'($)* 1234#"#)#$*%&!"#$%&#'().6%&27#!&/!(89(6&6%/+,-**!"#$"%&'.6%&27#!&/:6!&2%#.6/.+,-*!"#!$%&'+,-** / &!)#$*%&0 ' 1234#"#)#$*%& 6'!"#/012()*+34 Archface-U bigdatashare share bigdatashare Archface-U 6. Archface-U iarch-u P2P Archface-U A 26240007. [1] Allen, R. and Garlan, D.: Formalizing Architectural Connection, Proceedings of the 16th International Conference on Software Engineering, pp. 71 80 (1994). [2] Famelis, M., Salay, R. and Chechik, M.: Partial Models: Towards Modeling and Reasoning with Uncertainty, Proceedings of the 34th International Conference on Software Engineering, pp. 73 83 (2012). [3] Fukamachi, T., Ubayashi, N., Hosoai, S. and Kamei, Y.: Poster: Conquering Uncertainty in Java Programming, Proceedings of the 37th International Conference on Software Engineering, pp. 823 824 (201). [4] Magee, J. and Kramer, J.: State Models and Java Programs (1999). [] Perez-Palacin, D. and Mirandola, R.: Uncertainties in the Modeling of Self-adaptive Systems: A Taxonomy and an Example of Availability Evaluation, Proceedings of the th ACM/SPEC International Conference on Performance Engineering, pp. 3 14 (2014). [6] Ubayashi, N., Nomura, J. and Tamai, T.: Archface: A Contract Place Where Architectural Design and Code Meet Together, Proceedings of the 32nd International Conference on Software Engineering, pp. 7 84 (2010). [7] Java. Vol. 201, No. 21, pp. 1 8 (201). 8