STALLOY: A Spatio-Temporal Modelling Language

Alloy is a formal modeling language,by using model driven development method to complete the formal modeling and analysis of target systems,it can solve contradictory and ambiguity problems existing in traditional software development by applying infor-mal methods to describe the software specifications.By exposing the errors and defects in the system design,Alloy provides us with a well-structured software framework.And in the physical world,requirements of describing space and time are inevitable.However,Alloy fails to predefine the concept of time and space,which makes it impossible to model and analyze spatio-temporal systems.Therefore,it is urgent to construct a new language with the ability of modeling spatial and temporal properties.In spatio-temporal representation and reasoning,spatial logic provides a set of rela-tions to describe and determine whether there exists spatial connections between objects;temporal logic provides a variety of temporal operators to describe time relevant action.Based on the research and analysis of Alloy,spatial and temporal logic,we present a spatio-temporal modeling and analysis language STALLOY.The main construction pro-cess includes:1)we construct the spatial and temporal operators which follow the lan-guage specification in Alloy based on the characteristics of spatial and temporal logic,we apply the constructed operators to the regions to generate a set of spatial regions for spatio-temporal reasoning and calculus;2)we present a set of spatial relations to indicate whether there are spatial relations between spatial regions through combining region cal-culus with spatial operators,and apply temporal operators to first-order boolean logic to describe the properties of time related systems;3)By combing the spatio-temporal op-erators with relations,we extend the first-order relational logic in Alloy and propose a spatio-temporal modeling and analysis language STALLOY and its syntax and semantics on the basis of topological spatio-temporal model;4)we prove the computational com-plexity of spatio-temporal logic in STALLOY is EXPSPACE complete,and employ this logic to describe properties of spatio-temporal systems.After constructing STALLOY,we further propose the implementation of STALLOY tool by the following steps:1)based on the topological relation data model,we abstract the spatial regions into topological polygons,then provide the algorithm to implement spatial operators and relations;2)the implementation of temporal operators and relations is given after completing sequential relationship;3)we construct a STALLOY tool by applying our proposed spatial-temporal logic to the open source tool in Alloy.Finally,we use the train protection system as an example to demonstrate the model-ing and analysis capabilities of STALLOY.And through utilizing STALLOY and its tool,we complete the modeling,analysis and verification of spatial-temporal systems.