计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2012年
11期
2440-2449
,共10页
何炎祥%吴伟%陈勇%李清安%刘健博
何炎祥%吳偉%陳勇%李清安%劉健博
하염상%오위%진용%리청안%류건박
操作语义%形式化验证%内存模型%霍尔逻辑%内存安全
操作語義%形式化驗證%內存模型%霍爾邏輯%內存安全
조작어의%형식화험증%내존모형%곽이라집%내존안전
使用形式化方法对程序进行验证是保证软件可信的重要手段.对于像C语言这样的较低级的命令式语言可以直接对内存进行操作,对其操作语义或公理语义的形式化需要基于合适的内存模型.传统的字节内存模型可以很好地描述各种内存操作,但是无法保证安全性,同时使程序验证变得异常复杂.面向对象语言的内存模型则具有较高的抽象性,便于程序验证,但不适合描述低级的内存操作.结合字节内存模型和面向对象语言内存模型,提出一种安全的类型化的内存模型,既可用于对语义的形式化,也可用于基于霍尔逻辑的程序验证.此内存模型既允许指针算术、结构赋值、类型转换等内存操作,同时也可以有效减少因指针别名给程序验证带来的复杂度.基于Coq辅助定理证明工具,对内存模型进行了形式化实现和验证.
使用形式化方法對程序進行驗證是保證軟件可信的重要手段.對于像C語言這樣的較低級的命令式語言可以直接對內存進行操作,對其操作語義或公理語義的形式化需要基于閤適的內存模型.傳統的字節內存模型可以很好地描述各種內存操作,但是無法保證安全性,同時使程序驗證變得異常複雜.麵嚮對象語言的內存模型則具有較高的抽象性,便于程序驗證,但不適閤描述低級的內存操作.結閤字節內存模型和麵嚮對象語言內存模型,提齣一種安全的類型化的內存模型,既可用于對語義的形式化,也可用于基于霍爾邏輯的程序驗證.此內存模型既允許指針算術、結構賦值、類型轉換等內存操作,同時也可以有效減少因指針彆名給程序驗證帶來的複雜度.基于Coq輔助定理證明工具,對內存模型進行瞭形式化實現和驗證.
사용형식화방법대정서진행험증시보증연건가신적중요수단.대우상C어언저양적교저급적명령식어언가이직접대내존진행조작,대기조작어의혹공리어의적형식화수요기우합괄적내존모형.전통적자절내존모형가이흔호지묘술각충내존조작,단시무법보증안전성,동시사정서험증변득이상복잡.면향대상어언적내존모형칙구유교고적추상성,편우정서험증,단불괄합묘술저급적내존조작.결합자절내존모형화면향대상어언내존모형,제출일충안전적류형화적내존모형,기가용우대어의적형식화,야가용우기우곽이라집적정서험증.차내존모형기윤허지침산술、결구부치、류형전환등내존조작,동시야가이유효감소인지침별명급정서험증대래적복잡도.기우Coq보조정리증명공구,대내존모형진행료형식화실현화험증.
