Modeling Petri Nets Using Alloy

被引：0

作者：

Robles, Jonathan A. ^{[1
,2
]}

Solano, Geoffrey A. ^{[3
,4
]}

机构：

[1] Univ Philippines, Dept Comp Sci, Comp Secur Grp, Quezon City 1101, Philippines

[2] SeaChange Philippines Inc, Quezon City 1101, Philippines

[3] Univ Philippines, Dept Comp Sci, Quezon City, Philippines

[4] Univ Philippines Manila, Manila, Philippines

来源：

TENCON 2012 - 2012 IEEE REGION 10 CONFERENCE: SUSTAINABLE DEVELOPMENT THROUGH HUMANITARIAN TECHNOLOGY | 2012年

关键词：

Formal methods; Alloy; Petri nets;

D O I：

暂无

中图分类号：

TM [电工技术]; TN [电子技术、通信技术];

学科分类号：

0808 ; 0809 ;

摘要：

Petri net is a computational tool that is well-known in modeling various processes. Its formal semantics, graphical nature and expressiveness lend itself as a convenient model of computation for a wide-range of applications. On the other hand, Alloy is a declarative specification language used for expressing structural constraints and behavior in a software system. Alloy is heavily influenced by the Z notation on its mathematical aspects and Object Constraint Language on its syntax. An advantage of Alloy, however, is that its semantics bridges the gap between Z and object models, and shows how to give simple and robust meaning to widely used forms, such as navigation expressions and object model diagrams. This paper demonstrates how Petri nets and its properties and behavior can be specified using Alloy.

引用

页数：6