What Petri Nets Oblige Us to Say Comparing Approaches for Behavior Composition
We identify and demonstrate a weakness of Petri Nets (PN) in specifying composite behavior of reactive systems. Specifically, we show how, when specifying multiple requirements in one PN model, modelers are obliged to specify mechanisms for combining these requirements. This yields, in many cases, over-specification and incorrect models. We demonstrate how some execution paths are missed, and some are generated unintentionally. To support this claim, we analyze PN models from the literature, identify the combination mechanisms, and demonstrate their effect on the correctness of the model. To address this problem, we propose to model the system behavior using behavioral programming (BP), a software development and modeling paradigm designed for seamless integration of independent requirements. Specifically, we demonstrate how the semantics of BP, which define how to interweave scenarios into a single model, allow for avoiding the over-specification. Additionally, while BP maintains the same mathematical properties as PN, it provides means for changing the model dynamically, thus increasing the agility of the specification. We compare BP and PN in quantitative and qualitative measures by analyzing the models, their generated execution paths, and the specification process. Finally, while BP is supported by tools that allow for applying formal methods and reasoning techniques to the model, it lacks the legacy of PN tools and algorithms. To address this issue, we propose semantics and a tool for translating BP models to PN and vice versa.
Thu 18 MayDisplayed time zone: Hobart change
11:00 - 12:30 | Software verificationJournal-First Papers / NIER - New Ideas and Emerging Results / Technical Track / DEMO - Demonstrations at Meeting Room 106 Chair(s): Youcheng Sun The University of Manchester | ||
11:00 15mTalk | Data-driven Recurrent Set Learning For Non-termination Analysis Technical Track | ||
11:15 15mTalk | Compiling Parallel Symbolic Execution with Continuations Technical Track Guannan Wei Purdue University, Songlin Jia Purdue University, Ruiqi Gao Purdue University, Haotian Deng Purdue University, Shangyin Tan UC Berkeley, Oliver Bračevac Purdue University, Tiark Rompf Purdue University Pre-print | ||
11:30 15mTalk | Verifying Data Constraint Equivalence in FinTech Systems Technical Track Chengpeng Wang Hong Kong University of Science and Technology, Gang Fan Ant Group, Peisen Yao Zhejing University, Fuxiong Pan Ant Group, Charles Zhang Hong Kong University of Science and Technology Pre-print | ||
11:45 15mTalk | Tolerate Control-Flow Changes for Sound Data Race Prediction Technical Track Shihao Zhu State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,China, Yuqi Guo Institute of Software, Chinese Academy of Sciences, Beijing, China, Long Zhang Institute of Software, Chinese Academy of Sciences, Yan Cai Institute of Software at Chinese Academy of Sciences | ||
12:00 7mTalk | TSVD4J: Thread-Safety Violation Detection for Java DEMO - Demonstrations Shanto Rahman University of Texas at Austin, Chengpeng Li University of Texas at Austin, August Shi University of Texas at Austin | ||
12:07 7mTalk | What Petri Nets Oblige Us to Say Comparing Approaches for Behavior Composition Journal-First Papers Achiya Elyasaf Ben-Gurion University of the Negev, Tom Yaacov Ben-Gurion University of the Negev, Gera Weiss Ben-Gurion University of the Negev Link to publication DOI | ||
12:15 7mTalk | A Novel and Pragmatic Scenario Modeling Framework with Verification-in-the-loop for Autonomous Driving Systems NIER - New Ideas and Emerging Results Dehui Du East China Normal University, Bo Li East China Normal University, Chenghang Zheng East China Normal University |