Rev | Line | |
---|
[11] | 1 | $Id: README,v 1.1 1998/09/18 14:26:52 abel Exp $ |
---|
| 2 | |
---|
| 3 | Production Cell: |
---|
| 4 | |
---|
| 5 | This examples was obtained from: |
---|
| 6 | |
---|
| 7 | @InBook{Lindne94, |
---|
| 8 | author = {Thomas Lindner}, |
---|
| 9 | title = {Case Study "Production Cell": A Comparative Study in Formal |
---|
| 10 | Software Development}, |
---|
| 11 | chapter = 2, |
---|
| 12 | publisher = {FZI}, |
---|
| 13 | year = 1994, |
---|
| 14 | pages = {9,21} |
---|
| 15 | } |
---|
| 16 | |
---|
| 17 | It models the control of a plant in which a crane, two conveyor belts, a |
---|
| 18 | rotating table, an articulated arm and a press are involved. The system is |
---|
| 19 | closed, that is, there are no inputs. |
---|
| 20 | |
---|
| 21 | The movement of all the pieces has been discretized and encoded. The number of |
---|
| 22 | latches that the FSM will have is strongly dependent on the resolution chosen |
---|
| 23 | for these encodings. That would be a possible way to obtain a more challenging |
---|
| 24 | problem out of the same example. A parametric description, with one parameter |
---|
| 25 | for each encoding would be ideal. |
---|
| 26 | |
---|
| 27 | The formulas verified in the model refer to the limitation in the mobility of |
---|
| 28 | the different parts (safety) as well as the continuous progress of the system. |
---|
| 29 | |
---|
| 30 | See prodcell.ctl for the detailed set of formulas. |
---|
| 31 | |
---|
| 32 | Author: Abelardo Pardo <abel@vlsi.colorado.edu> |
---|
Note: See
TracBrowser
for help on using the repository browser.