=Paper=
{{Paper
|id=Vol-1508/paper3
|storemode=property
|title=Behavioral Types for Space-aware Systems
|pdfUrl=https://ceur-ws.org/Vol-1508/paper3.pdf
|volume=Vol-1508
|dblpUrl=https://dblp.org/rec/conf/models/BlechH15
}}
==Behavioral Types for Space-aware Systems==
https://ceur-ws.org/Vol-1508/paper3.pdf
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.