The Application of Model Checking in Validating Information System Software Security

被引：0

作者：

Liu Xin ^{[1
]}

Cai Wandong ^{[1
]}

机构：

[1] Northwestern Polytech Univ, Xian, Peoples R China

来源：

2011 INTERNATIONAL CONFERENCE ON COMPUTERS, COMMUNICATIONS, CONTROL AND AUTOMATION (CCCA 2011), VOL III | 2010年

关键词：

software security; validation; model checking;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

This paper discusses the effectiveness of model checking in validating information system software security, and give the formal definition for these two properties. A model checking based security policy validation and verification method is proposed to validate the consistency and completeness for security policy. This method can also be used to generate a validation sequence. Finally, we'll discuss our availability and reliability of validation methods:

引用

页码：448 / 451

页数：4

共 50 条

[21] Software model checking without source code [J].

Chaki, Sagar ;

Ivers, James .

INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (03) :233-242

[22] Practical use of model checking in software development [J].

Myers, K ;

Dionne, K ;

Cruz, J ;

Vijay, V ;

Dunlap, S ;

Gluch, DP .

IEEE SOUTHEASTCON 2002: PROCEEDINGS, 2002, :21-27

[23] Interface grammars for modular software model checking [J].

Hughes, Graham ;

Bultan, Tevfik .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2008, 34 (05) :614-632

[24] Abstract modeling formalisms in software model checking [J].

College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing ;

210016, China ;

不详 ;

210037, China .

Jisuanji Yanjiu yu Fazhan, 7 (1580-1603) :1580-1603

[25] Interface grammars for modular software model checking [J].

University of California .

ACM Int. Symp. Softw. Test. Anal., 2007, (39-49) :39-49

[26] Process Rewrite Systems for Software Model Checking [J].

Touili, Tayssir .

2013 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE), 2013, :15-22

[27] Model Checking Aspectual Pervasive Software Services [J].

Abeywickrama, Dhaminda B. ;

Ramakrishnan, Sita .

2011 35TH IEEE ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 2011, :253-262

[28] Model Checking of Software Safety Based on LLBMC [J].

Du, Ye ;

Kang, Xin ;

Zhang, Ya-Hang ;

Wang, Lu-Yuan ;

Li, Mei-Hong .

INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND COMMUNICATION ENGINEERING (CSCE 2015), 2015, :85-90

[29] Abstracting Security-Critical Applications for Model Checking in a Model-Driven Approach [J].

Borek, Marian ;

Stenzel, Kurt ;

Katkalov, Kuzman ;

Reif, Wolfgang .

PROCEEDINGS OF 2015 6TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE, 2015, :11-14

[30] Supporting automated containment checking of software behavioural models using model transformations and model checking [J].

Muram, Faiz U. L. ;

Tran, Huy ;

Zdun, Uwe .

SCIENCE OF COMPUTER PROGRAMMING, 2019, 174 :38-71

← 1 2 3 4 5 →