Friday, September 26, 2008


New lecturer going on a new topic called flexibility with formal methods. Flexibility is how thing are connected. Optimize communication processes. Modular machines. Plug and play dream of hardware.

Cannot do plug and play if you are not sure a out the behavior of the hardware. Smulatuon is not exhaustive enough because of only gives you one scenario from the entire state space.

Ladder diagrams to programme PLD. Petri nets.

Model checking of a controller. Take the desired CCS and the model and check all states. Designing air travel. Gap between the concept and implementation. Control system has control and plant. Including the plant also simplified the state space.

Net Condition Event Systems: NCES is a modular language. Tokens flow along arcs. Transition and condition ports. Interfaces between models of plant and controller ate the same as between the real controller and real plant.

Assume the plant is just behavior and has no intelligence. Just a physical model. To handle plants with continuous behavior, use hybrid automata. Include differential equations. Reachability space is infinite. Common method is to discertize the state space.

Visual Verifier.  Up to chapter two of ViVe. Draw the reachability for an NCES diagram.

Composed and transmitted from my iPod Touch

No comments: