Dynamically Updating Controllers from Specification Changes

Dynamic Updates

Example

Getting Started

Step-by-Step Guide

system specification PickAndPlaceRobotSpecification {

 domain PickAndPlaceSystem // domain model package name

 define Controller as controllable
 define Arm as uncontrollable
 define TableSensor as uncontrollable
 define DepositBelt as uncontrollable

 non-spontaneous events {
   Controller.arrivedAtBelt,
   Controller.arrivedAtTable
 }

 collaboration PickAndPlaceBehavior {

   static role TableSensor ts
   static role Controller c
   static role Arm a
   static role DepositBelt belt

   /* S1 */ 
   specification scenario ArmPickUpPieceAndMoveToBelt { 
     message ts->c.pieceArrived()
     strict requested wait until [c.armAtTable]
     message strict requested c->a.pickUp()
     message strict requested c->belt.startWindBelt()
     message strict requested c->a.moveToBelt()
   }

   /* needed to know when pick-up is possible */ 
   specification scenario SetArmAtTableFalse {
     message c->a.moveToBelt()
     message strict requested c->c.setArmAtTable(false)
   }

   /* needed to know when pick-up is possible */ 
   specification scenario SetArmAtTableTrue {
     message a->c.arrivedAtTable()
     message strict requested c->c.setArmAtTable(true)
   }

   /* S2 */ 
   specification scenario ArmReleasePieceOntoBelt {
     message a->c.arrivedAtBelt()
     message strict requested c->a.release()
   }

   /* S3 */ 
   specification scenario ArmMoveToTableAfterRelease {
     message c->a.release()
     message strict requested c->a.moveToTable()
   }

   /* S4 */
   specification scenario ReleaseAfterArrivedAtBelt {
     message a -> c.arrivedAtBelt()
     message strict requested c -> belt.stopWindBelt()
     message strict requested c -> a.release()
   }
   
   /* S5 */
   requirement scenario ReleaseOntoBeltAfterStartWind {
     message c -> belt.startWindBelt()
     message strict requested c -> belt.stopWindBelt()
   }

   /* A1 */ 
   assumption scenario ArmMoveFromTableToBelt {
     message c->a.moveToBelt()
     message strict requested a->c.arrivedAtBelt()
   }

   /* A2 */ 
   assumption scenario ArmMoveFromBeltToTable {
     message c->a.moveToTable()
     message strict requested a->c.arrivedAtTable()
   }
   
   /* A3 */ 
   assumption scenario NoNewPieceArrivesBeforeArmPicksUp {
     message ts->c.pieceArrived()
     message strict c->a.pickUp()
   }
 }
}