Line | |
---|
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.