1 1 1 Checking the Consisteny between Requirements Specification Documents and Regulations Abstract: When developers check the consistency between requirements specification documents and regulations by Model checking, they need state transition models of the documents and logic specifications of regulations. Moreover, they have to know which words in documents correspond to words in applicable regulations in respect of meaning so that they create logic specifications. In this paper, we propose a technique to reason the meaning of words in requirements specification documents by using co-occurrence restrictions in case frames and to create state transition models based on the reasoned meaning and logic specifications of applicable regulations. These specifications are created from these reasoned meaning and logic expressions which contain case frames as factors and express regulations. Our proposal is evaluated with a case study. Keywords: Use case description, Model checking, Case grammar 1. [1] [2] 1 Tokyo Institute of Technology [3] [4] 1
[5] 6 4 8 4 2 3 4 5 6 7 2. 2.1 [6] (, :, :, : ) [7] 2.2 1 [3] *1 (, : x, :, : y) (, : x, : ) (, : x, :, : y) (, : x, : ) [2] s, a s AF a (, :, :, : ) *1 2
シナリオの順序 状態遷移, 変数の導出 [ 鈴木 ] 状態遷移モデル モデル検査器 ユースケース 格構造 格構造 + 単語の概念 整合性判定 : 要求文の概念特定 : 規則の論理式の具体化 検査式 単語辞書 格フレーム辞書 概念階層辞書 規則の論理式 言語資源 1 1 2.3 [8] 3. 3.1 1 is-a [8] [9] 3
3.2 3.1 is-a 3 2 概念階層 制度 組織 事業者 単語システム 格フレーム辞書 抽象物 個人情報 住所取る 住所 学問 取得 学ぶ 動詞主格 ( ガ ) 深層格 ( ヲ ) 源泉格 ( カラ ) 学ぶ人 組織学問人 組織 人 客 顧客 動詞主格 ( ガ ) 深層格 ( ヲ ) 源泉格 ( カラ ) 取る人 組織具体物人 組織 2 W C W C 2 { w w c } 1 c [9] c w rep { c w rep c } w rep rep is-a C C 2 is-a. c v case d rest f = (c v, case d: rest,... ) (1) F 2 2 f 1 f 1 = (, :, :, : ) (2) m f f 1 m f1 ( ) 2 c c c &! 3.3. w v cases: w n,.... (, :, :, : ) w n. w v w v F wv = { (c v, cased: rest,... ) F w v c v } (3) w v = 2 2. w n (case d, rest) case d = m f (case s ) case d rest case s w n 4
{( : : ), ( : : ), ( : : )}, (4) {( : : ), ( : : ), ( : : )} (5). w n rest w n c r s [10] s min{s(r a, c), s(r b, c)} (r = r a & r b ) max{s(r a, c), s(r b, c)} (r = r a r b ) s(r, c) = 1 s(c r, c) (r =! c r ) s(c r, c) (r = c r ) (6) c r s(c r, c) 1 (c c r ) s(c r, c) = 1/(d min + 1) () 0 (c c = c p ) d(c c, c p ) = 1 (c p c c ) 1 + d () s(c r, c) c r c is-a c r c is-a 1 (8) is-a d d { d(c c, c p ) c p c p } d min { d(c c, c ) c c c c p c } c c c p c c 2 s(, ) = 1/(2 + 1) = 0.67 s (7) (8) slots = {(w n, case d, rest, cs, score) i } (9) score cs 2 (4) (5) (9) (,, { }, 1) (,, { }, 1/3). score f = slots k=1 score k slots + 1 (10) (10) 1 score 1 (10) 3/4(0.75) 2.33/4(0.58) score f (11) 3.4 (w v, c v, score f, slots) (11) f 1 = (c 1, case1 i : rest 1 i,... ), f 2 = (c 2, case2 j : rest 2 j,... ) c 1 = c 2 case 1 i case 1 i = case2 j case2 j c (s(rest 1 i, c) = 1 s(rest 2 j, c) = 1) (12) f 2 f 1 (11) f i cs (11) CS i i CS 1 CS n n CS i = CS i = {FALSE} f i 3.2 rep CS i 5
3 (rep(c v ), cased: rep(c rep ),... )}) (13) c rep (9) cs (, :, :, : ) AF (, :, :, : ) {(, :, :, : )}, {(, :, :, : )}, (, :, :, : ) AF(, :, :, : ) 4. 5.2 3 4 4 [2] 2 5 (14), (15), (16) * 2.3 * NuSMV *2 CTL Cabocha *3 5. 5.1 *2 http://nusmv.fbk.eu/ *3 https://code.google.com/p/cabocha/ AG((, :, :, : ) &!(, :, : ) AF (, :, :, : ) (, :, : )) AG ((, :, : ) AF (, :, : )) (14) (15) 6
1 EDR 270000 410000 13000 EDR * 61(9) 59(17) 10(1) * ( ) 2 2 2 1 1 2 2 0 0 2 0 1 1 AG((, :, :, : ) AF((, :, :, : ) &(, :, : ) (, :, :, : ))) (16) EDR [11] EDR 1 5.3 4/8(0.50), 4/6(0.66) 2 (16) (15) 5.4 1 (14) AG(((, :, :, : )&!FALSE) (17) AF((, :, :, : ) FALSE)) 5.5 [4] 15, 144, include 3 16, 146, 5 7
6. KNP *4 KNP Web [12] KNP [13] [14], [15] Sinnig [16] Sinning 7. [1] Otto, P. N. and Antón, A. I.: Addressing Legal Requirements in Requirements Engineering, Proc. RE, pp. 5 14 (2007). [2] Saeki, M., Kaiya, H. and Hattori, S.: Detecting Regulatory Vulnerability in Functional Requirements Specifications, Proc. ICSOFT, Vol. 1, pp. 105 114 (2009). [3] Saeki, M. and Kaiya, H.: Supporting the Elicitation of Requirements Compliant with Regulations, Proc. CAiSE, pp. 228 242 (2008). [4],, Vol. 2010, No. 17, pp. 1 8 (2010). [5],, 2014 pp. 76 84 (2014). [6] Fillmore, C. J.: Some problems for case grammar, Monograph series on languages and linguistics, Vol. 24, pp. 35 56 (1971). [7] Bird, S., Klein, E. and Loper, E.: O Reilly Japan, Inc. (2010). [8] (2012). [9],, Vol. 113, No. 489, pp. 25 30 (2014). [10] Russell, S. and Norvig, P.: Artificial Intelligence: A Modern Approach, Prentice Hall Press, 3rd edition (2009). [11] EDR. [12] Web Vol. 2006, No. 1, pp. 67 73 (2006). [13],, Vol. 31, No. 2, pp. 175 181 (1990). [14] May, M. J., Gunter, C. A. and Lee, I.: Privacy APIs: Access Control Techniques to Analyze and Verify Legal Privacy Policies, 19th IEEE Computer Security Foundations Workshop, pp. 85 97 (2006). [15] Ingolfo, S., Jureta, I., Siena, A., Perini, A. and Susi, A.: Nòmos 3: Legal Compliance of Roles and Requirements, Proc. ER, pp. 275 288 (2014). [16] Sinnig, D., Chalin, P. and Khendek, F.: LTS Semantics for Use Case Models, Proc. SAC, pp. 365 370 (2009). *4 http://nlp.ist.i.kyoto-u.ac.jp/index.php?knp 8