...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>The Journal of Systems and Software >Formally analyzing software architectural specifications using SAM
【24h】

Formally analyzing software architectural specifications using SAM

机译：使用SAM正式分析软件架构规范

获取原文
获取原文并翻译 | 示例
   

获取外文期刊封面封底 >>

       
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In the past decade, software architecture has emerged as a major research area in software engineering. Many architecture description languages have been proposed and some analysis techniques have also been explored. In this paper, we present a graphical formal software architecture description model called software architecture model (SAM). SAM is a general software architecture development framework based on two complementary formalisms―Petri nets and temporal logic. Petri nets are used to visualize the structure and model the behavior of software architectures while temporal logic is used to specify the required properties of software architectures. These two formal methods are nicely integrated through the SAM software architecture framework. Furthermore, SAM provides the flexibility to choose different compatible Petri net and temporal logic models according to the nature of system under study. Most importantly, SAM supports formal analysis of software architecture properties in a variety of well-established techniques―simulation, reachability analysis, model checking, and interactive proving. In this paper, we show how to formally analyze SAM software architecture specifications using two well-known techniques―symbolic model checking with tool Symbolic Model Verifier, and theorem proving with tool STeP.
机译：在过去的十年中，软件体系结构已成为软件工程的主要研究领域。已经提出了许多体系结构描述语言，并且还探索了一些分析技术。在本文中，我们提出了一种称为软件体系结构模型（SAM）的图形化形式化软件体系结构描述模型。 SAM是一个通用的软件体系结构开发框架，它基于两种互补的形式主义-Petri网和时态逻辑。 Petri网用于可视化结构并为软件体系结构的行为建模，而时间逻辑用于指定软件体系结构所需的属性。通过SAM软件体系结构框架可以很好地集成这两种形式的方法。此外，SAM还提供了根据正在研究的系统的性质灵活选择不同的兼容Petri网和时间逻辑模型的灵活性。最重要的是，SAM支持使用各种公认的技术对软件体系结构属性进行形式化分析，包括模拟，可及性分析，模型检查和交互式证明。在本文中，我们展示了如何使用两种众所周知的技术来正式分析SAM软件体系结构规范：使用工具Symbolic Model Verifier进行符号模型检查以及使用工具STeP进行定理证明。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号