Formal Modeling and Analysis of Time-and Resource-Sensitive Simple Busineb Procebes

Kazuhiro Ogata, Thapana Chaimanont, Min Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

1 Scopus citations

Abstract

A time-and resource-sensitive simple businebproceb (TR-SBP) consists of a finite set of finite series ofactivities that have timing and resource constraints. A TRSBPseems simple, but its analysis needs to consider whatare not explicitly mentioned as activities and may introducea non-negligible number of intermediate states. In this sense, the analysis has similarities with security protocol analysisthat needs to consider intruders. We formalize TR-SBPs asa round-based model, and describe how to specify and analyzeformalized TR-SBPs (Formal TR-SBPs) using Alloy.

Original languageEnglish
Title of host publicationProceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1-10
Number of pages10
ISBN (Electronic)9781509002900
DOIs
StatePublished - 15 Mar 2016
Event2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015 - Wuhan, Hubei, China
Duration: 16 Nov 201519 Nov 2015

Publication series

NameProceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015

Conference

Conference2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015
Country/TerritoryChina
CityWuhan, Hubei
Period16/11/1519/11/15

Keywords

  • Alloy
  • Time
  • busineb proceb
  • formal analysis
  • resource
  • round-based model

Fingerprint

Dive into the research topics of 'Formal Modeling and Analysis of Time-and Resource-Sensitive Simple Busineb Procebes'. Together they form a unique fingerprint.

Cite this