Abstract
Applications described by Sequential Function Chart (SFC) often being critical, we have studied the possibilities of program checking. In particular, physical time can be handled by SFC programs using temporisations, that’s why we are interested in the quantitative temporal properties. We have proposed a modeling of SFC in timed automata, a formalism which takes time into account. In this modeling, we use the physical constraints of the environment. Verification of properties can be carried out using the model-checker Kronos. We apply this method to SFC programs of average size like the one of the controlling part of the production cell Korso. The size of the programs remaining however a limit, we are studying the means of solving this problem.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1994.
N. Bouteille, P. Brard, G. Colombari, N. Cotaina, and D. Richet. Le GRAFCET. “Cépadués Édition”, Toulouse, France, 1992.
C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool Kronos. In R. Alur, T. Henzinger, and E.D. Sontag, editors, DIMACS Workshop on Verification and Control of Hybrid Systems, pages 208–219. LNCS 1066, Springer-Verlag, 1995.
C. Ghezzi, D. Mandrioli, S. Morasca, and M Pezzé. A unified high-level Petri net formalism for time-critical systems. IEEE Transactions On Software Engineering, 17(2):160–172, February 1991.
N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor, 5th Conference on Computer-Aided Verification, pages 333–346. LNCS 697, Springer-Verlag, 1993.
N. Halbwachs, F. Lagnier, and C. Ratel. Programming and verifying real-time system by means of the synchronous data-flow language Lustre. IEEE Transactions on Software Engineering, 18(9):785–793, September 1992.
T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems. Information and Computation, 111(2):193–244, 1994.
P. Le Guernic, T. Gautier, M. Le Borgne, and C. Le Maire. Programming real time applications with Signal. Proceedings of the IEEE, 79(9):1321–1336, 1991.
P. Le Parc, D. L’Her, J.L. Scharbarg, and L. Marcé. Le Grafcet revisité á l’aide d’un langage synchrone flot de données. Technique et Science Informatiques, 17(1):63–86, January 1998.
C. Lewerentz and T. Lindner. Case study ‘production cell’: A comparative study in formal specification and verification. In C. Lewerentz and T. Lindner, editors, Formal Development of Reactive Systems: Case Study Production Cell, pages 1–54. LNCS 891, Springer-Verlag, 1995.
D. L’Her. Modélisation du Grafcet temporisé et vérification de propriétés temporelles. PhD thesis, Université de Rennes 1 (France), September 1997.
X. Nicollin, J. Sifakis, and S. Yovine. Co mpiling real-time specifications into extended automata. IEEE Transaction on Software Engineering. Special Issue on Real-Time Systems, 18(9):794–804, 1992.
J.S. Ostroff. Automated Verification of Timed Transition Models. In G. Goos and J. Hartmanis, editors, Workshop on Automatic Verification Methods for Finite State Systems, pages 247–256. LNCS 407, Springer-Verlag, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
L’Her, D., Le Parc, P., Marcé, L. (1999). Proving Sequential Function Chart Programs Using Automata. In: Champarnaud, JM., Ziadi, D., Maurel, D. (eds) Automata Implementation. WIA 1998. Lecture Notes in Computer Science, vol 1660. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48057-9_13
Download citation
DOI: https://doi.org/10.1007/3-540-48057-9_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66652-3
Online ISBN: 978-3-540-48057-0
eBook Packages: Springer Book Archive