Pushlogic is a scripting language originally developed as part of the CMI Pebbles Project. The Pushlogic root page is here.
Although designed for highly-dynamic populations of devices, sensors, actuators and applications, today Pushlogic is suited to domains where the population is infrequently changed, such as an aircraft, automobile or oil refinery. This is because the current generation of automated proof tools take a long time to run, starting from tens of seconds and ranging into tens of hours.
This work is relevant at the point of design or extension to closed systems of sensors, actuators and applications. It is useful for designers of industrial plant control and automotive and aerospace fieldbus systems. It is especially useful where systems must dock with each other, such as when two sets of train carriages join to become a single train.
Industry requires joined up tool flows. Companies can rarely afford abrupt changes in the way they make their product. Although we have proposed Pushlogic High Level as an authoring language for new applications in this environment, we are equally as keen on tapping into existing tool flows to explore automated proofs of correctness.
In many of our target areas, UML and application domain-specific language (DSL) tools are used for design entry and mockup. In some companies, these are sufficiently integrated with backend flows for embedded firmware to be generated for the controllers. In other companies, manual recoding is used. Either way, it is widely-agreed that feature interactions must be detected as early as possible, which means working off machine-readable design sketches.
If you are an industrial designer with a problem in this space, please get in touch with mailto:David Greaves.
(C) 2006 University of Cambridge. END.