摘要
将统一建模语言 (UML )的面向对象可视化设计与代数规范语言 Cafe OBJ的形式描述相结合 ,对冗余磁盘阵列 (RAID)系统中的并发特性进行建模、分析和规范 .提供了 RAID系统的清晰结构 ,以此来弥补形式化规范语言的不足 ,规范软件设计过程 ,保证程序的正确性 .
The formal specification approach provides the mechanisms for system modeling, specifying and verifying in parallel. But the high abstract, complex expression, bad readability and reusability block it from further development. To make up for the limitation of formal approach, this paper presented a formal object-oriented method, which integrates CafeOBJ algebra specification language with the objected-oriented UML visible tools to model and verify the concurrent dynamic characteristics of redundant arrays of inexpensive disks (RAID) control system.
出处
《上海交通大学学报》
EI
CAS
CSCD
北大核心
2001年第2期245-249,共5页
Journal of Shanghai Jiaotong University
基金
国家自然科学基金!资助项目 (6 0 0 740 11F0 3)