Behavioral Types for Space-aware Systems Jan Olaf Blech Peter Herrmann RMIT University Norwegian University of Science and Technology Melbourne, Australia Trondheim, Norway {janolaf.blech@rmit.edu.au} {herrmann@item.ntnu.no} Abstract—Behavioral types for space-aware systems are pro- • Type compatibility checking — as known from types posed as a means to facilitate the development, commissioning, of imperative programming languages, e.g., checking maintenance, and refactoring of systems with cyber-physical whether we can add an integer to a float — with space- characteristics. In this paper, we particularly introduce the formal definition of behavioral types that are associated with aware behavioral types associated to components. system components in order to specify their expected behavior. • Subtyping allows the replacement of a component with As application domain, we concentrate on systems from industrial a certain behavioral type t by another component that automation that encompass recurring behavior. has a subtype t0 of type t. We base subtyping on spatial geometric refinement that can be checked automatically. I. I NTRODUCTION • Type composition is necessary to infer types of com- ponents that are composed of existing components with In the industrial automation domain, many systems consist known types. of physically distributed components that cooperate with each In addition, we want to ensure other by carrying out recurring behavioral patterns. A typical • Type conformance, i.e., the question whether a component example is a state-of-the-art assembly line consisting of a really behaves according to its specification: the geomet- series of robots that build complex articles like cars. To work ric spatial behavioral type. correctly, the behaviors of the components need to fulfill various software and physical behavioral aspects that can be A. Motivating Examples quite diverse and may comprise, for instance, communication Loading robot: Figure 1 shows two pictures of a robot protocols, heat emission or spatial occupation (e.g., a robot interacting with a moving device. The robot and the device adding a part to a car must perform trajectories such that the have spatial behaviors, i.e., their positions in space change car’s carriage is not damaged). during time. At various points on the time scale, that we To handle the complexity and diversity of specifying com- call timepoints, they physically occupy certain spaces that ponent and system behaviors, we introduce space-aware be- can be characterized by coordinates in a geometric coordinate havioral types that allow us to capture both software and system. On the one hand, we like to ensure using space- physical aspects. As with types in traditional programming aware behavioral types that the robot does not collide with the languages, e.g., primitive datatypes and their composition, moving device. On the other one, we also want to guarantee the behavioral types can be used to eliminate error sources that the robot grip is coming very close to the device in order already at the development time of software systems. This to avoid that articles are damaged while being loaded onto the is analog to classical static type checks performed by a device. compiler. Furthermore, we can use the behavioral types to The robot consists of three segments and a tool that are eliminate runtime errors. This resembles dynamic type checks attached to each other via joints. Each of the four robot that, in many programming languages, are performed when components has an individual spatial behavior relative to the accessing pointers that reference data of types which cannot be parts it is attached to. As depicted on the left side of Fig. 1, statically determined. Behavioral types also provide additional this spatial behavior can be expressed with a space-aware information about components which can be used for tool- behavioral type that encodes the movement of a robot part based operations that allow the discovery of components and over time. Typically, the behavioral description of each type the dynamic reconfiguration of systems. is relative to a distinct point in the coordinate system. For The behavioral types introduced in this paper are applicable example, multiple instances of the tool may have the same on different scales such as to express the interaction of the type, but may be deployed independently in different locations various parts of a single robot or to specify collaboration (e.g., segments 1 and 3). Likewise, we can use a behavioral aspects between different sites (cf. [8]). The limitation to type expressing the behavior of the moving device. recurring behavior makes it possible to verify behavior by The right side of Fig. 1 shows the composition of the types checking only a finite number of situations which eases the from the robot’s components into a single type representing use of highly automatic verification tools. Our approach makes the behavior of the overall robot. The composed type for the it possible to check the following features of a type system: robot takes the relative spatial movements of the segment and W\SH!MRLQW DOW W\SH!VHJPHQW W\SH!MRLQW DOW W\SH!VHJPHQW W\SH!WRRO W\SH!MRLQW W\SH!URERW W\SH!VHJPHQW W\SH!PRYLQJGHYLFH FRPSDWLELOLW\ W\SH!EDVLV W\SH!PRYLQJGHYLFH Fig. 1. Behavioral types for a robot c3 is also a robot arm, possibly of the same kind as c1, c2 that performs the same rotational movement around a different center point. In consequence, the behavioral type of c3 may be the same as the one of c1 which, however, refers to another center point. c1 A typical type checking problem is the decision whether c3 the system composed of c1 and c2 can collide with c3. For type checking, we compute the least common multiple of the cycle times for each of the three components and compare for each time point whether a collision may occur. The use of time points instead of time intervals requires that the spatial behavior at each time point is a safe approximation of the behavior during the adjacent time intervals. We will discuss this later in detail. Fig. 2. Spatial behavior of rotating robot arms B. Related Work The idea to use well defined specifications that define the tools to each other into account. To verify that the robot does interfaces of software component systems, has been made not collide with the moving devices but that its grip comes popular by the design-by-contract approach for software com- sufficiently close, we can apply the composed type of the ponents [31]. More recent work comprises specification and robot instead of the four simple ones referring to its parts. contract languages for component-based systems that have The spatial verifications are carried out by type checking of the been studied in the context of web services. Process algebra- composed robot type and the one of the moving device. Using like languages and associated techniques are studied in [11], the subtyping feature, we can even replace robot segments by [16]. Another algebraic approach to service composition is other ones without needing to repeat the type checking proofs presented in [18]. In [27], so-called External State Machines of safety properties as long as the replaced segments are in (ESMs) are used to specify the interface behavior of functional certain relations with the original ones. software building blocks. The ESMs do not only facilitate Rotating robot arm: Another example of a robot com- the integration of the building blocks into their environment position is depicted in Figure 2. Here, three components are but make also compositional model checking of the building shown: c1 is a robot arm. It performs a circular movement blocks possible. around a center point and features a reference point at the outer Behavioral types have been studied as interface automata end that turns counterclockwise. This behavior is captured [1] for software components and in the Ptolemy II project [30] using a space-aware behavioral type. Another component c2 for the software part of real-time systems. Further, their use as also carries out a counterclockwise circular movement albeit means for behavioral checks at runtime for component-based with a smaller radius. This is also encoded in a space-aware systems was investigated in [2]. behavioral type. c2 gets attached to c1 via the reference We proposed a behavioral type system in [9]. In [6], ensur- point. By type composition, we can create a behavioral type ing behavioral type correctness at runtime using techniques modeling the joint behavior of c1 and c2. from runtime verification was discussed in the context of Java/OSGi-based applications. Moreover, we studied compat- hold at which timepoint. Due to the recurrent nature of ibility checking in [7]. This paper also features a solution the behavior, we have to observe only a finite number of for behavioral type coercion for a highly restricted class of timepoints. In Sect. II-A we describe the basic formalism of behavioral types. Furthermore, we have applied a behavioral our behavioral type definitions and introduce certain templates types concept to the software part of automation control facilitating the use of our method. Thereafter, we discuss the systems [37] which can be seen as a precursor of the work constructors and composition operators in Sect. II-B. In the presented here. Providing a format for spatial behavioral types remainder of this section we justify our modeling choices. and means to reason about it is a new contribution of this paper. A. Behavioral Descriptions Specification of spatial properties has been studied using We use simple logic-based descriptions to define abstract process algebra-like formalisms [13], [14]. A type system datatypes. These behavioral descriptions can be composed of based on this formalism was introduced in [12] for con- the following operators and predicates: currency and resource control. The author presents typing • Logical operators: ∧, ∨, and ¬ as well as abbreviations rules and automatic type checking which is not a focus here. such as −→ and i∈I . V Moreover, a verification tool has been developed to check • Predicates that characterize timepoints. This includes properties based on this formalism in [15]. In contrast, we expressions such as timepoints modulo a cycle time — are interested in developing a solution that fits for industrial after which the behavior is repeated — and time intervals. robots and related machinery. Therefore, we restrict ourselves • Predicates characterizing events. In addition to the space- to the checking of recurrent behavior in geometric space and aware aspects one can also use events to specify software concentrate us on tailoring a formalism and compliant check- interaction protocols [9]. ing techniques for this particular domain. Contracts between • Predicates indicating nodes and edges in a graph struc- components with a cyber-physical flavour have been studied ture. in the SPEEDS project [3], [4], [20]. Here, the contracts also • Predicates indicating occupation of geometric space. take behavior in the form of a transition system into account. • Parameters defining the ownership of space occupation. In [32] contracts for avionic components are studied. Here, spatial occupation behavior is associated with a Reasoning about spatial and geometric constraints is de- certain component that owns the occupied space. scribed in, e.g., [5], [25]. A particularly important applica- Our way to associate space occupation with ownership tion domain is robot path planning which has been studied allows us to specify various spatial properties of a component for decades (e.g., [26], [29]). Spatial types are also used in separation. As already mentioned, examples for such prop- for databases, e.g., to manage geometric objects [21] or in erties that may all refer to the same physical component C, Geographic Information Systems [36]. A challenge of these may be C’s physical occupation of space, the distribution of approaches is to guarantee that a reasonable subset of the heat emitted by C, and the range over which C may broadcast spatial logic is decidable and, of course, that realistic system wireless communication messages. These properties can be models can be checked in an acceptable period of time modeled by separate predicates that all use C as their owner. (e.g., see decidability results in [17]). Logic approaches for In consequence, the individual properties can be separately hybrid systems (e.g., [19], [34], [35]) provide comprehensive verified by type checking which is carried out based on two languages and tools for describing cyber-physical systems. In different approximation approaches: contrast to these works, our focus is stronger aligned with the industrial automation domain and the use as a behavioral type • Overapproximation means to consider a geometric space system. The time and geometry focus on the reasoning side of that is at least as large as the one that is factually covered our framework can be complemented by a topological view. by an owner. This fits to properties like the physical This has advantages in areas such as security analysis [33]. occupation of space or the distribution of heat. As we will show below, the approach presented here fits • Underapproximation refers to a geometric space that is well to the existing verification technique BeSpaceD [10] that at most as large as the one factually covered. We can use already proved that it can be used to check spatial properties it, for example, to check broadcasting ranges. of various systems (see [22], [23], [24]). The two approaches are closer described in Sect. III. Templates: Behavioral descriptions encoding a compo- C. Overview nent of the industrial automation / robot domain can follow Section II introduces our space-aware behavioral types. The the templates shown in Fig. 3. The specification features underlying semantics and related behavioral types features are a conjunction over implications. Each implication refers to discussed in Sect. III. An evaluation is featured in Sect. IV certain conditions that hold at a certain timepoint and in the followed by a conclusion in Sect. V. presence of events. The conditions can be, for instance, aspects referring to the spatial occupation of a geometric object. Each II. S PACE - AWARE B EHAVIORAL T YPES aspect itself is constructed as predicates of the behavioral In general, we describe spatiotemporal behavior for the description language introduced above. It primarily features industrial automation domain by defining which properties constraints on space such as conjunctions of predicates that t = 1 ∧ (¬) event E0 ∧ ... ∧ (¬) event En −→ Space Occupation Aspect 1 ∧ ... ∧ Space Occupation Aspect m ∧ ... ∧ t = 1 ∧ (¬) event E0 ∧ ... ∧ (¬) event En −→ Space Occupation Aspect h ∧ ... ∧ Space Occupation Aspect j ∧ ... ∧ t = cycletime ∧ (¬) event E0 ∧ ... ∧ (¬) event En −→ Space Occupation Aspect 1 ∧ ... ∧ Space Occupation Aspect m ∧ ... ∧ t = cycletime ∧ (¬) event E0 ∧ ... ∧ (¬) event En −→ Space Occupation Aspect h ∧ ... ∧ Space Occupation Aspect j Fig. 3. Template for a behavioral description indicate the occupation of space for a geometric object. A 1) A behavioral description bd may be accompanied by the space occupation aspect is either classified as an over- or an cycle time ct, after which the behavior is repeated to underapproximation. form a geometric spatial behavioral type using the tuple The template specifies spatial behavior up to the timepoint (bd, ct) referring to finishing a recurrent behavior cycle. After the cycle time, the behavioral description is repeated. This, however, 2) An extended definition features a geometric offset go does not necessarily always result in the same behavior, which is a point in the geometric space. Likewise, space- since events may be different. Having a cycle time is a aware behavioral types allow to shift the starting time typical feature in industrial automation and a key characteristic of a cycle by a time offset to in order to allow the reuse of Programmable Logic Controllers (PLC) used to control of the behavioral description for a component that may automation facilities (e.g., the IEC 61131-3 and IEC 61499 be started with a delay. The spatial and starting time standards) and for controlling industrial robots. impacts of the behavioral description can be described Behavioral descriptions may be specified by developers by the following tuples: manually. However, typical descriptions can comprise several (bd, go, ct), (bd, to, ct) and (bd, go, to, ct) thousand cases. Thus, a preferable way is to specify a system in a simulation or development tool and generate the behav- 3) A component that features a behavior in time and space ioral description automatically. We have successfully done this may be attached to a joint device of another compo- using the model-based engineering tool Reactive Blocks [28] nent where this joint device has its own spatiotemporal as described in [23], [24]. behavior. This relative movement of a component to another is captured in the following type definition: B. Type Constructors and Composition A type may feature a set RP of reference points Type constructors use behavioral descriptions and additional through which other components may be attached to information to create a space-aware behavioral type. We it and a behavioral description is provided with each present two kinds of space-aware behavioral types. Primitive reference point. For instance, the segments and the tool space-aware behavioral types are often used to capture the of the robot introduced in Sect. I-A are attached to behavior of a single atomic component, whereas composed each other via reference points. Each reference point space-aware behavioral types are typically applied to capture exhibits its own spatiotemporal behavior that depends the behavior of composed systems. However, composed types on both, the physical placement of the reference point may also be applied to characterize different aspects of a single as well as the behavior of the overall component. In atomic component and a primitive type may be used to capture the type constructor, we model the relation between the behavior of a composed system, when no detailed behavior reference points and their behavioral descriptions by of subcomponents is available or it is not necessary to describe the function 7→ mapping all elements of set RP to the that separately. set BD of all possible behavioral descriptions. Thus, if Basic space-aware behavioral types: We define three bdi ∈ BD is the behavioral description of a reference different kinds for the primitive behavioral types: point rpi ∈ RP , the formula 7→ (rpi ) = bdi holds which we express as rpi 7→ bdi for convenience. The type is made up of the behavioral type tt of the tool and the constructor is defined as follows: types at1 , at2 , at3 of the three robot arm segments. The four types can be nested in the following way: (bd, RP, 7→, ct) (at1 , {rpat1 }, The behavioral description used in the reference point rpat1 7→ (at2 , {rpat2 }, must only describe the movement of a single point in rpat2 7→ (at3 , {rpat3 }, rpat3 7→ (tt)) relation to time and events. ) Composed space-aware behavioral types: The behavior ) of multiple components can be combined, e.g., to form new Using our introduced definition, the behavioral type of components or to define alternative types. A way to combine each segment type ati with a behavioral description abi behavior types syntactically is type composition. Its semantics has the form: is highlighted in the following: 1) The union type + provides an alternative between two (abi , {rpati }, rpati → rpbrpati ) different space-aware behavioral types gbt and gbt0 each where rpbrpk refers to the behavior of a reference point defined as one of the three types introduced above: rpk thereby removing the nested structure. gbt + gbt0 Our notion of behavioral types takes the intended semantics into account, i.e., the behavior in space and time. Different syn- As an example, the intended semantics — a behavioral tactic type definitions which may be grouped into equivalence alternative — of a union of two space-aware behavioral classes may exist for the same space-aware behavioral type. types is given below (lcm denotes the least common For instance, by using the symmetry of the union operator multiple): in type composition or the symmetry of ∧, we can construct (bd, ct) + (bd0 , ct0 ) , ((bd ∨ bd0 ), lcm(ct, ct0 )) syntactically different type definitions for the same type. 2) Compositions as expressed by the operator × correspond III. S EMANTICS OF S PACE - AWARE B EHAVIORAL T YPES to record types in programming languages: To facilitate the verification that objects occupy a certain geometric space in an area, we can use subtyping of the be- gbt × gbt0 havioral types of these objects. As described in Sect. II-A, ver- Semantically, that corresponds to the following operation ification of spatial properties can be performed based on both, on the behavioral description level: overapproximation and underapproximation. This is consid- ered by distinguishing subtyping between overapproximation- (bd, ct) × (bd0 , ct0 ) , ((bd ∧ bd0 ), lcm(ct, ct0 )) refinement aspects and underapproximation-refinement as- Furthermore, as in records, we support an implementa- pects. A space-aware behavioral type T 0 is a subtype of tion that maps names to behavioral descriptions. This another type T if and only if the following conditions hold allows us to have record-like field descriptors. for each spatial aspect and each shared timepoint t: 3) Composing structures of components attached to ref- • For overapproximation-refinement aspects, the space oc- erence points, like in the robot example depicted in cupation at t specified in T 0 is geometrically included in Fig. 1, usually leads to lengthy nested behavioral de- T . Thus, overapproximation-oriented spatial proofs (e.g., scriptions. To simplify these definitions, we offer non- collision avoidance) that were carried out for a physical nested type constructors for such structures. The non- component represented by T also hold for a “smaller” nested variant does not have to be attached to a base one described by T 0 . component such it does not need to feature a cycle • For underapproximation-refinement aspects, the space time. The simplified constructor can be used if a struc- occupation at t specified in T is geometrically included ture consisting of composed components is modeled by in T 0 . So, underapproximation proofs (e.g., broadcast the basic space-aware behavioral type gbt of kind 3, ranges) done for T hold also for a “larger” T 0 . i.e., gbt , (bd, RP, 7→, ct). We also introduce the set • For both, overapproximation-refinement and underappro- GBT that features the geometric spatial behavior in ximation-refinement aspects hold, that if T comprises the remainder of the nested structure, as well as the unbound reference points, T 0 incorporates the same un- function → mapping the reference points rpi ∈ RP bound reference points, which show an identical behavior. in the composed structure to their respective behaviors Subtyping imposes a partial order relation between the gbti ∈ GBT , i.e., rpi → gbti . The resulting behavioral space-aware behavioral types since according to our definition type is syntactically defined in the following way: the following properties hold: • Reflexivity: A type is its own subtype since an occupied (gbt, RP, →) space includes itself. To illustrate this, we regard our motivating example from • Antisymmetry: For aspects refined by overapproximation Sect. I-A and Fig. 1. The composed type for the robot holds that if the space occupied according to T 0 is geometrically included in the one of T but not identical, behavioral then there is at least a point in space that is occupied by types T but not by T 0 . Thus, the space of T is not included in extraction the one of T 0 and, in consequence, T is not a subtype of cycle times checking T 0 with respect to overapproximation. The argumentation iterative / behavioral selection for underapproximation is analog. description parallel 0 00 • Transitivity: If T is a subtype of T and T a subtype of abstraction behavior 0 T with respect to overapproximation, then the occupied time / aspect space according to T 00 is included in the one defined spatial boxes transformation by T 0 and that one is included in the one according representation to T . Thus, the occupied space defined for T 00 is also point included in the one specified in T such that T 00 is also a representation subtype of T . An analogous deduction can be drawn for underapproximation. overlapping inclusion check check It is possible to construct a lattice based on this partial order for a fixed number of aspects. The type ⊥ is a subtype of Fig. 4. Checking type compatibility and subtyping all other types. Here, all overapproximation-refinement aspects are occupying zero space all the time, while underapproxi- mation-refinement aspects occupy all the space all the time. more fine grained verification conditions as we discuss in the In contrast, all other types are subtypes of the > element. Thus, following. underapproximation-refinement aspects occupy zero space all B. Making Behavioral Descriptions Checkable the time, while overapproximation-refinement aspects occupy all the space all the time. Our modeling style allows for very rich specifications de- scribing quite complex systems. Checking these specifications IV. B EHAVIORAL T YPE C HECKING AND E VALUATION would demand to treat a state space that would exceed the time and memory limits of the type checking algorithm introduced In this section, we discuss means to decide the compatibility above. In the following, we present some steps allowing to of system components based on their behavioral types. abstract complex specifications into checkable ones such that A. Type Compatibility Checking Algorithm our type compatibility checking and subtyping algorithms can be used. To guarantee that the abstractions do not falsify For two space-aware behavioral types with cycle times ct1 the verification results, they have to preserve the transitivity, and ct2 , we perform space-aware behavioral type checking in reflexivity, and antisymmetry properties introduced in Sect. III. the following way: The abstraction consists of an order of operations that is 1) We calculate the least common multiple of ct1 and ct2 depicted in Figure 4 (see also [10]): that we name ct. 1) From time intervals to timepoints: Time interval-based 2) For all time points t between 0 and ct we perform the descriptions are transformed into timepoint-based de- following steps: scriptions by using safe approximations of geometric a) Retrieve for both behavioral types all relevant spatial behavior of adjacent time intervals at the time- spatial information expressed by the behavioral points. descriptions bd1 and bd2 at timepoint t. 2) Extraction of relevant behavioral information: Be- b) Decide possible overlappings between the behav- SpaceD provides functions that are based on time and ioral descriptions bd1 and bd2 by regarding the pos- spatial aspects and provide sub-descriptions for the sibly occupied space for all underapproximation- relevant behavior which are defined on the inductive refinement aspects. Here, an overlapping must oc- structure of the behavioral descriptions. cur, for each spatial aspect. Otherwise, the types 3) From segments to boxes: Parts of robots may be de- are incompatible. scribed by segments or other geometric objects. Seg- c) Decide additional possible overlapping between ments have a cylindric shape with a radius, a length, and spatial information of bd1 and bd2 by regarding an orientation. For fast and easy checking, we convert the possibly occupied space for all overapproxima- segments and other geometric objects into box-based tion-refinement aspects. Here, no overlapping must approximations. Boxes are defined by an upper left front occur for any spatial aspect. Otherwise, the types and a lower right rear coordinate that are both expressed are incompatible. by their respective x, y and z axes of the coordinate The algorithm is carried out using the checker BeSpaceD [10] system. Figure 5 shows a variant of the second example that, depending on the geometry used, converts the spatial from Sect. I-A in which the line representations of the information and property into a SAT or an SMT problem. For three robot components are replaced by a number of that, BeSpaceD breaks the geometric constraints down into boxes representing the space covered. As long as the abstract class Invariant; abstract class ATOM extends Invariant; case class OR (t1 : Invariant, t2 : Invariant) extends Invariant; case class AND (t1 : Invariant, t2 : Invariant) extends Invariant; case class NOT (t : Invariant) extends Invariant; case class IMPLIES (t1 : Invariant, t2 : Invariant) extends Invariant; ... case class TimePoint [T](timepoint : T) extends ATOM; case class TimeInterval [T] (timepoint1 : T, timepoint2 : T) extends ATOM; case class Event[E] (event : E) extends ATOM; ... case class Occupy3DBox (x1 : Int, y1: Int, z1 : Int, x2 : Int, y2 : Int, z2 : Int) extends ATOM; case class OccupySegment3D (x1 : Int, y1 : Int, z1 : Int, Fig. 5. Box-based abstraction of rotating robots x2 : Int, y2 :Int, z2 : Int, radius : Int) extends ATOM; case class Occupy3DPoint (x:Int, y:Int, z: Int) boxes cover all the space of the three components, this extends ATOM replacement is a safe overapproximation. (It would be a safe underapproximation if all space represented by the Fig. 6. Some Scala definitions boxes was covered by the components.) 4) Automata and spatial behavior: The behavior of our components can be modeled using automata with a language Scala which facilitates the break down and conver- cyclic control flow. Here, we describe possible transi- sion of behavioral descriptions. tions and states encountered as events that are part of Behavioral descriptions are provided as abstract data types the behavioral description. called Invariant. We chose this name since logical de- 5) From boxes to spacepoints: Behavioral descriptions us- scriptions are supposed to capture the abstract behavior of a ing geometric boxes can be broken down into descrip- component during its entire lifetime. For look and feel, we tions that contain geometric points, so-called space- provide an excerpt in Fig. 6. Some logical operators, predicates points. For example, a cube with a side length of 10 may for time and events and geometric occupation of time are be broken down into 10 · 10 · 10 = 1000 spacepoints. In shown. The description language is more expressive than the the behavioral description, each spacepoint is described subset used for space-aware behavioral types, e.g., time only using a predicate. In spite of this enlargement of the needs to be a type with a partial order (parameter T) whereas behavioral representation, we can check the spacepoints in our semantics definitions above we used integers. speedily since points from different behavioral descrip- In the following, we discuss two features of the implemen- tions are comparable without further interpretation. tation: 6) Checking of overlappings and inclusion with points: We Type system features: Using the type constructors above use hash-sets for checking overlappings and inclusion of with the behavioral specifications, our type checking algorithm two descriptions. For overlappings, we insert points from invoking the BeSpaceD tool allows us to check (i) space- one description into the hash-set and check whether the aware behavioral type compatibility and (ii) whether a space- points of the second description are already in the hash- aware behavioral type is a subtype of another one. Note, that set. For inclusion, we insert points from one description behavioral descriptions can look different, but may describe and check whether all points from the other description the same type. Our framework is able to decide both subtyping are indeed included in the hash-set. and type compatibility, since we exhaustively simulate possible 7) SMT and other approaches: In addition to comparing behavior bounded by the a cycle time. In cases, where the geometric representations on a point level, we have behavioral descriptions use elements that we cannot check, developed SMT encodings of geometric objects that are we may still derive an order of types based on checkable more efficient for large sets of points [10]. Furthermore, spatial aspects. For all non-checkable aspects, we assume checking of point-wise overlappings and inclusion can safe approximations. Hence, a type for which the behavioral also be performed in BeSpaceD using a SAT solver. specification is uncheckable for all aspects, is equivalent to ⊥. Speed of type checking: We implemented the space-aware C. Implementation behavioral types checking as described above. Checking can A first implementation of BeSpaceD and space-aware be- be done in acceptable time, e.g., checking two types with a havioral types exists. It is done in the functional programming cycle time of 1000 different timepoints and 15000 spacepoints for the first resp. 20000 spacepoints for the second behavioral [14] L. Caires and L. Cardelli. A Spatial Logic for Concurrency (Part II). description was done in between seven and eight seconds on Theoretical Computer Science, 322(3) pp. 517–565, September 2004. [15] L. Caires and H. Torres Vieira. SLMC: a tool for model checking an Intel core i5 running 2.8 GHz with 8 GB RAM using Mac concurrent systems against dynamical spatial logic specifications. Tools OS 10.8.4. and Algorithms for the Construction and Analysis of Systems. Springer, 2012. V. C ONCLUSION [16] G. Castagna, N. Gesbert, L. Padovani. A theory of contracts for Web services. ACM Trans. Program. Lang. Syst. 31(5), 2009. We presented behavioral types as a concept for space- [17] S. Dal Zilio, D. Lugiez, C. Meyssonnier. A logic you can count on. aware systems facilitating the development, commissioning, Symposium on Principles of programming languages, ACM, 2004. maintenance, and refactoring of systems with cyber-physical [18] J. L. Fiadeiro, A. Lopes. Consistency of Service Composition. Fun- damental Approaches to Software Engineering (FASE), vol. 7212 of characteristics. Using a robot system, we motivated, formally LNCS, Springer, 2012. defined and discussed their applicability. [19] G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. The approach is intended to be used in industrial automa- Ripado, A. Girard, T. Dang, O. Maler. SpaceEx: Scalable Verification of Hybrid Systems. Computer Aided Verification (CAV’11), 2011. tion. Facilities in the domain typically operate using cycles, [20] S. Graf, R. Passerone, and S. Quinton. Contract-based reasoning for after which behavior is repeated. For example, a robot in an component systems with rich interactions. Embedded Systems Develop- assembly line may perform the same movement and operation ment, ser. Embedded Systems, vol. 20, pp. 139-154, Springer, 2014. [21] R.H. Güting, R. Hartmut, and M. Schneider. Realm-based spatial data on a workpiece over and over again with slight variations based types: the ROSE algebra. The VLDB JournalThe International Journal on the color of a work piece. Our behavioral descriptions were on Very Large Data Bases 4.2 (1995): 243–286. designed with that kind of behavior in mind. [22] F. Han, J. O. Blech, P. Herrmann, and H. Schmidt. Model-based Engineering and Analysis of Space-aware Systems Communicating via Moreover, we believe that the use of behavioral type-like IEEE 802.11. In 39th Annual International Computers, Software & specifications of cyber-physical systems is especially impor- Applications Conference (COMPSAC), pages 638–646, IEEE Computer, tant for remote collaboration of engineering teams. Ongoing 2015. [23] F. Han, J. O. Blech, P. Herrmann, H. Schmidt. Towards Verifying Safety work in this direction comprises our collaborative engineering Properties of Real-Time Probabilistic Systems. Formal Engineering project [8] with a focus on remote handling of industrial approaches to Software Components and Architectures, 2014. installations in the Australian outback (such as mining sites) [24] P. Herrmann, J.O. Blech, F. Han, H. Schmidt. A Model-based Toolchain to Verify Spatial Behavior of Cyber-Physical Systems. In 2014 Asia- or for oil rigs. Pacific Services Computing Conference (APSCC), IEEE Computer. [25] D. Hirschkoff, É. Lozes, D. Sangiorgi. Minimality Results for the Spatial R EFERENCES Logics. Foundations of Software Technology and Theoretical Computer [1] L. de Alfaro, T.A. Henzinger. Interface automata. Symposium on Science, vol 2914 of LNCS, Springer, 2003. Foundations of Software Engineering, ACM , 2001. [26] S. Kambhampati and L.S. Davis. Multiresolution path planning for [2] F. Arbab. Abstract Behavior Types: A Foundation Model for Compo- mobile robots. Volume 2 , Issue: 3, Journal of Robotics and Automation, nents and Their Composition. Formal Methods for Components and IEEE 1986. Objects. vol. 2852 of LNCS, Springer-Verlag, 2003. [27] F. A. Kraemer and P. Herrmann. Automated Encapsulation of UML [3] A. Benveniste, B. Caillaud, A. Ferrari, L. Mangeruca, R. Passerone, and Activities for Incremental Development and Verification. In Model C. Sofronis, Multiple viewpoint contract-based specification and design. Driven Engineering Languages and Systems (MoDELS), LNCS 5795, Formal Methods for Components and Objects. Springer-Verlag, 2008. pages 571–585. Springer-Verlag, 2009. [4] A. Benveniste, B. Caillaud, D. Nickovic, R. Passerone, J.-B. Raclet, P. [28] F. A. Kraemer, V. Slåtten and P. Herrmann. Tool Support for the Reinkemeier et al.. Contracts for System Design, INRIA, Rapport de Rapid Composition, Analysis and Implementation of Reactive Services. recherche RR-8147, Nov. 2012. Journal of Systems and Software, 82(12):2068–2080, 2009. [5] B. Bennett, A. G. Cohn, F. Wolter, M. Zakharyaschev. Multi- [29] J.-C. Latombe. Robot Motion Planning. Kluwer Academic Publishers, Dimensional Modal Logic as a Framework for Spatio-Temporal Rea- 1991. soning. Applied Intelligence, Volume 17, Issue 3, Kluwer Academic [30] E.A. Lee, Y. Xiong. A behavioral type system and its application in Publishers, November 2002. ptolemy ii. Formal Aspects of Computing, 2004. [6] J. O. Blech. Ensuring OSGi Component Based Properties at Runtime [31] B. Meyer. Applying ”Design by Contract”. Computer, 25, 10, pp. 40–51, with Behavioral Types. Model-Driven Engineering, Verification, and IEEE, October 1992. Validation, 2013. [32] P. Nuzzo, H. Xu, N. Ozay, J. Finn, A. Sangiovanni-Vincentelli, R. [7] J. O. Blech. Towards a Framework for Behavioral Specifications of OSGi Murray, A. Donz, and S. Seshia, ”A contract-based methodology for Components. Formal Engineering approaches to Software Components aircraft electric power system design,” IEEE Access, vol. 2, pp. 1-25, and Architectures. Electronic Proceedings in Theoretical Computer 2014. Science, 2013. [33] L. Pasquale, C. Ghezzi, C. Menghi, Ch. Tsigkanos, and B. Nuseibeh. [8] J. O. Blech, I. Peake, H. Schmidt, M. Kande, S. Ramaswamy, Su- Topology aware adaptive security. In Proceedings of the 9th International darsan SD., and V. Narayanan. Collaborative Engineering through Symposium on Software Engineering for Adaptive and Self-Managing Integration of Architectural, Social and Spatial Models. Emerging Systems, pp. 43–48. ACM, 2014. Technologies and Factory Automation (ETFA), IEEE, 2014. [34] A. Platzer. Differential dynamic logic for hybrid systems. Journal of [9] J. O. Blech and B. Schätz. Towards a Formal Foundation of Behavioral Automated Reasoning, vol. 41.2: 143–189, Springer, 2008. Types for UML State-Machines. UML and Formal Methods. Paris, [35] A. Platzer, J.-D. Quesel. KeYmaera: A Hybrid Theorem Prover for France, ACM SIGSOFT Software Engineering Notes, August 2012. Hybrid Systems (System Description). International Joint Conference [10] J. O. Blech and H. Schmidt. Towards Modeling and Checking the Spatial on Automated Reasoning, pp. 171–178, LNCS 5195, Springer, 2008. and Interaction Behavior of Widely Distributed Systems. Improving [36] P. Rigaux, M. Scholl, and Agnes Voisard. Spatial databases: with Systems and Software Engineering Conference, Melbourne, 2013. application to GIS. Morgan Kaufmann, 2001. [11] M. Bravetti, G. Zavattaro. A theory of contracts for strong service [37] M. Wenger, J. O. Blech and A. Zoitl. Behavioral Type-based Monitoring compliance. Mathematical Structures in Computer Science 19(3): 601– for IEC 61499. To appear in Emerging Technologies and Factory 638, 2009. Automation (ETFA), IEEE, 2015. [12] L. Caires. Spatial-behavioral types for concurrency and resource control in distributed systems. Theoretical Computer Science, Elsevier, 2008. [13] L. Caires and L. Cardelli.A Spatial Logic for Concurrency (Part I). Information and Computation, Vol 186/2 November 2003.