Simulation, Model Checking, and Execution of Activity Models

TL;DR

This paper explores how activity models can be used for simulation, verification, and execution, highlighting the importance of model distinctions and the role of continuous-time modeling in system behavioral analysis.

Contribution

It demonstrates the use of DEVS and Constrained-DEVS for validating and verifying activity models, emphasizing the impact of temporal characteristics on behavioral specifications.

Findings

Continuous-time models reveal limitations and strengths in activity modeling.

DEVS enables validation of activity model simulations.

Constrained-DEVS facilitates verification of activity models.

Abstract

This paper presents our findings for using activity modeling for simulation (validation), model checking (verification), and execution purposes. Each is needed to tackle system complexity and further research into behavioral modeling. We argue different models implicate different understandings and expectations. We emphasize some distinctions with demonstrations using the Discrete Event System Specification with an exemplary model. In particular, the continuous-time base in models helps observe some inherent limitations and strengths in acquiring each capability. The temporal characterization of input, output, and state, or the lack thereof, is at the core of developing behavioral specifications. We use DEVS to arrive at the capability of validating simulations for activity models. We use Constrained-DEVS for the verification of activity models. We show how some executions can be derived, whether from the specification itself or with considerations for simulation and model checking.