Abstract
The structure of data and processes to manage information are both important
aspects of information systems. Nevertheless, most existing modeling languages
focus either on one or the other. Languages that focus on data often neglect that
data is manipulated by processes, while languages tailored for processes ignore the structure of the data.
In this paper, we present an approach to model and analyze information systems that combines data models with process models by means of an automated
theorem prover. In the proposed approach, data models are used to express the
structure and constraints of data, while Petri nets with identifiers define the processes together with a specification on how transitions manipulate the data. Through the use of an automated theorem prover, a transition is checked whether its manipulation is valid given the constraints imposed by the data model. Our approach allows specifying an information system over a spectrum of balances between data and process constraints. This spectrum is exemplified with an educational institute as a running example. The approach is supported with a proof-of-concept implementation using CPN-tools and the automated theorem prover E.
aspects of information systems. Nevertheless, most existing modeling languages
focus either on one or the other. Languages that focus on data often neglect that
data is manipulated by processes, while languages tailored for processes ignore the structure of the data.
In this paper, we present an approach to model and analyze information systems that combines data models with process models by means of an automated
theorem prover. In the proposed approach, data models are used to express the
structure and constraints of data, while Petri nets with identifiers define the processes together with a specification on how transitions manipulate the data. Through the use of an automated theorem prover, a transition is checked whether its manipulation is valid given the constraints imposed by the data model. Our approach allows specifying an information system over a spectrum of balances between data and process constraints. This spectrum is exemplified with an educational institute as a running example. The approach is supported with a proof-of-concept implementation using CPN-tools and the automated theorem prover E.
| Original language | English |
|---|---|
| Place of Publication | Utrecht |
| Publisher | UU BETA ICS Departement Informatica |
| Number of pages | 18 |
| Publication status | Published - 2018 |
Publication series
| Name | Technical Report Series |
|---|---|
| Publisher | UU Beta ICS Department Informatica |
| No. | UU-CS-2018-004 |
| ISSN (Print) | 0924-3275 |