|
Published Articles >> Table of Contents >> Abstract
Second IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'96)
p. 230
Formal verification for distributed real-time control: periodic Producer/Consumer
S. Koppenhoefer, Lab. d'Inf. Tech., Swiss Federal Inst. of Technol., Lausanne, Switzerland
J. Decotignie, Lab. d'Inf. Tech., Swiss Federal Inst. of Technol., Lausanne, Switzerland
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICECCS.1996.558419
Send link to a friend
| Abstract |
|
The Producer/Consumer (P/C) has been used to model communication in networks. The model states that in a system there is a producer of a given information and one or more consumers of this information. With this model different kinds of communication failures may occur. In this paper with the help of the adapted synchronous model (ASM), we show two methods for formally verifying the necessary conditions to avoid buffer overwrites in the P/C model. Specifically, we explore the constraints on communication parameters in distributed periodic control and more generally, we demonstrate how behavioral properties can be analyzed using formal methods.
|
 Additional Information
|
Index Terms- formal verification; distributed real-time control; periodic Producer/Consumer; verification; adapted synchronous model; communication parameters; distributed periodic control; model; communication in networks; communication failures; buffer overwrites
Citation:
S. Koppenhoefer, J. Decotignie,
"Formal verification for distributed real-time control: periodic Producer/Consumer,"
iceccs,
p. 230,
Second IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'96),
1996
|
|
