Overview

In this chapter (file), we explain how to use ROSCoq to program an iRobot Create. Our program receives requests to navigate to specific positions and computes appropriate commands for the robot. This programs forms will be a software agent in a distributed system consisting of 3 agents, as shown in the figure: The hardware agent represents the iRobot create hardware and its ROS drivers. It was defined in the previous chapter. The request to navigate comes from the external agent. In the next chapter, we will prove upper bounds on how close the robot will end up to the requested position. To do this proof, we use the axiomatization of the hardware agent. If you have an iRobot Create, you will be able to run the program on the robot. The Coq program can be extracted to Haskell and linked with a shim that actually handles the sending and receiving of messages. Coq guarantees that the program will behave as proved, unless our axiomatization of the robot was incorrect. Before getting into the details of the specification of the entire distributed system in ROSCoq, let us first look at the core of the navigation program.

To move to the target position, the robot first turns towards it and then moves forward. Because a robot may not be able to physical achieve any arbitrary angular linear speed, we let the user specify the desired speeds. By adjusting the duration of rotation and linear motion, we can make the robot go anywhere. The two variable respectively denote the user specified rotational(angular) and linear speed.

To control the duration of rotation, the program inserts a delay between the command to start turning and the command to stop turning. The shim in Haskell can only support a finite resolution for the time requests. The variable below is used to specify the resolution of the timer. Formally, 1/delRes is the resolution of the timer. The current Haskell shim is based on the threadDelay function of Haskell, whose resolution is 1 microseconds. Hence delRes will be instantiated with 1000000. However, we choose to make our program and proofs generic over that value.

The meaning of the 2 parameters below will be explained while explaining the program.

Here is the program. For a detailed explanation, please refer to Section 4.2 of the ROSCoq paper

Specifying the whole cyber-physical system system.

The above program sends 4 commands to the iRobot create device driver. The behaviour of the robot on the receipt of such commands is specified in the axiomatization of the robot. To be able to prove that the robot will end up at a place close to the position requested by the external agent, we have to specify the whole cyber-physical system that it is a part of, or at least its relevant parts. For example, we have to specify the agents of the distributed system, and the fact that the messages sent by the software agent are received by the robot device driver.

Topics

Like the Robot Operating System (ROS), ROSCoq uses a publish-subscribe approach to communication between agents of a distributed system. Agents can publish messages to named topics without knowing about who are receiving them. Similarly, agents can subsctibe to topics without knowing who is publishing them. As explained in the previous chapter, the icreate driver subscribes to a designated topic, and acts on the messages specifying the linear and angular velocities for the robot. To specify a Cyber-physical System (CpS) in ROSCoq, one specifies a type denoting the collection of topics used for communication. This type must be an instance of the TopicClass typeclass.

In this application, we use 2 topics. The VELOCITY topic is used the software agent to send the linear and angular velocity commands to the robot hardware agent. The TARGETPOS topic is used by the external agent (see Fig. in Sec. 1) to send the cartesian coordinates of the target position (relative to the robot’s current position) to the software agent.

TopicClass the type to have decidable equality

The TopicClass also needs the payload type for eqch topic.

The type Topic will serve as an implicit parameter of the type Message. A message is just a dependent pair of a topic and its payload type. Here is an example usage.

Collection of Agents.

To be able to holistically reason about a CpS, we have to specify the collection of agents and the physical model of the cyber-physical system. One has to then specify the behavior of each agent in a mutually independent way. All of this is achieved by specifying an instance of CPS. We will see how to build one for our example. First, we need a type to denote the collection of agents. Each member of the type below denotes an agent (vertical downward arrow) in the message sequence diagram near the top of this page. Also, below they appear in the same order as they appear in the figure above.

Decidable equality is a requirement of the CPS typeclass

The typeclass CPS also needs a function that specifies the list of topics subscribed and published by each agent. A TopicInfo is a pair of lists. The first member is the list of subscribed topics. The second member is the list of published topics. This list cannot be changed at runtime. When actually running a software agent, the Haskell shim uses the ROS (Robot Operating System) API to subscribe to each topic in the first member of TopicInfo. The software agent will then be invoked on any ROS message received on the subscribed topics.

Physical Model

Now that we have defined the the collection of agents, we have to specify the behvior of each agent in a mutually independent way. However, the behavior of hardware devices such as sensors and actuators cannot be specified without modeling the evolution of the relevant physical quantities (e.g. the ones they measure or influence). The first argument of CPS, which is implicit, a a type denoting the physical model of the cyber-physical system. As described in Sec. 2 of the ROSCoq paper, A physical model is a type that specifies how each relevant physical quantities evolved over time, and the physical laws governing that evolution. In this example, there is only one robot (iRobot Create), and the physical quantities are the physical quantities relevant to that robot where specified in the type iCreate. So that type will serve as our physical model. If there were, say 2 robots, the physical model could be the type iCreate * iCreate

Semantics of Agents

Now we specify the behavior of each agent. Recall from section 4 of the ROSCoq paper that each agent is specified as a relation between how the physical quantities evolved over time and how the sequence of events at the agent. In the above message sequence diagram, events are denoted by either a start or an end of a slanted arrow. Such slanted arrows denote flight of messages. Using the Context keyword, we assumed the type Event which denotes the collection of all events. We also assumed that the type Event is an instance of the EventType typeclass. This typeclass enables us to use many functions events. For example, we can use eLoc to get the location of an event. For more details, please see the definition of the type EventType (just clicking it should take it to its definition), or see Sec. 3 of the ROSCoq paper

Hardware Agent

It is more sensible to change the type to QNonNeg as the value certainly does not represent time. However, the coercion QT2Q does not work then

Software Agent

External Agent

The network model.

To specify a CPS, we need to specify its network model In this example, we assume that the network reliably delivers messages.

Putting it all together.