The contents below reflect the state of ROSCoq at the submission of the ITP15 paper. For the latest and greatest, please visit the ROSCOQ wiki at github.

Physical Aspects :

core.v : defintion of time (Time, QTime), continuous functions over time (TContR), derivatives w.r.t. time (isDerivativeOf and many lemmas about bounds on functions based on bounds on their derivatives at rational values of time (e.g. TDerivativeLBQ, TDerivativeUBQ).
CartCR.v : conversion between cartesian and polar coordinates, proofs of correctness of the conversions
CartIR.v : definition of coordinates after that the axes are rotated such that the new X axis is in the direction of a given point (rotateOriginTowardsF). DerivativerotateOriginTowards2 characterizes the derivative of the new coordinates in terms of the derivatives of the old coordinates

Cyber Aspects :

MsgHandler.v : definiton of a message handler with state, lemmas characterizing its state and output after a handling a finite sequence of mesages
roscore.v : definition of topics, messages and software agents

Cyber-physical Aspects :

ROSCyberPhysicalSystem.v : definition of events, causal ordering, semantics of agents, derivation of semantics of a software agent from its Coq program (SwSemantics), definition and correctness proofs of utility functions which find latest payload on a topic
robots/icreate.v : specification of an increate robot. It incudes the definition of its physical model, and the specification of the behavior of its behaviour as a hardware agent.

Applications of the framework :

examples/iCreateMoveToLoc.v : instantiation of the above abstract definition of a CPS to specify running example of paper. It incudes the Coq program run by the software agent and a specification of the external agent. After specification, bounds are derived on how close the robot will be to the position it is asked to be at. Main lemmas are: ThetaEv2To3P, Ev3Y', Ev3X'DiffUb, and Ev3X'DiffLb
We used a ROSJava shim to run a specialization (robotProgramInstance) of the above Coq program on actual robots.
examples/train.v Before working on iCreate, we formalized a CPS representing the case of a hypothetical train traveling back and forth repeatedly between two stations. This CPS has 3 hardware agents : a proximity sensor (ProximitySensor) at each end of the train and a motor at the base for 1D motion. The software controller uses messages generated by the proximity sensor to reverse the direction of motion when it comes close to an endpoint. We proved that it will never collide with an endpoint (TrainSafe).