Abstract
Various methods are used to describe communication protocols. The search for suitable description methods for communication protocols in the 1980s yielded a broad range of approaches out of which some fundamental methods have crystallized. These methods constitute the basis of the semantic models of the various formal description techniques. Therefore we first consider the most important description methods in this chapter before we turn to the formal description techniques. From these, finite state machines, Petri nets, process calculi, and temporal logics have crystallized as the most important and most common ones. Apart from these methods, other approaches were also investigated, such as the use of grammars, data flow languages, and functional languages. They did not receive wider attention because they were not applied to real-life protocols. The use of high-level programming languages was considered likewise. Programming languages support the algorithmic description of protocol procedures as well as the generation of prototypes, but they usually do not possess a formally defined semantics. In addition, programming languages are primarily implementation languages and not specification languages. They often yield descriptions which are close to an implementation. For that reason, high-level programming languages are not used for protocol description. Many formal description techniques, however, use programming language features.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
State tables describe the states of the protocol entity interpreted as a finite state machine (see Section 7.4)
- 2.
The terms finite state machine and automaton are used synonymously below.
- 3.
iff – if and only if
- 4.
The letters S and R stand for Sender- and Receiver-SAP, respectively.
References
Anderson, J.A.: Automata Theory with Modern Applications. Cambridge University Press, Cambridge, 2006.
Bause, F.; Kritzinger, P.S.: Stochastic Petri Nets - An Introduction to the Theory. Vieweg, Wiesbaden, 2002.
Billington, J.; Diaz, M.; Rozenberg, G. (eds.): Application of Petri Nets to Communication Networks. LNCS 1605. Springer, 1999.
von Bochmann, G.; Verjus, J.-P.: Some Comments on “Transition-oriented” vs. “Structured” Specification of Distributed Algorithms and Protocols. IEEE Transactions on Software Engineering SE-13 (1987) 4: 501 - 505.
Bowman, H.; Gomez, R.: Concurrency Theory. Springer, 2006.
Clarke, E.; Grumberg, O.; Peled, D.: Model Checking. MIT Press, Cambridge, 2000.
Emerson, E.A: Temporal and Modal Logic. In: van Leeuwen, J. (ed.): Handbook of Theoretical Computer Science. Elsevier Science, Amsterdam, pp. 997-1072, 1990.
Annual IFIP Working Conference on formal description techniques. In 1996 it was combined with PSTV (Protocol Specification, Testing and Verification). Today it belongs to the DISCOTEC conference series. Proceedings of the FORTE conference cited here are, for instance, [Gotz 96a], [Kim 01] and [Koni 03].
Girault, C.; Valk, R.: Petri Nets for Systems Engineering - A Guide to Modeling, Verification, and Applications, Springer, 2001.
Gordon, S.; Billington, J.: Analysing the WAP Class 2 Wireless Transaction Protocol Using Coloured Petri Nets. In: Nielsen, M; Simpson, D. (eds.): Application and Theory of Petri Nets 2000. LNCS 1825, Springer, pp. 207-226, 2000.
Gotzhein, R.: Temporal Logic and Applications - a Tutorial. Computer Networks and ISDN Systems, 24 (1992): 203 - 218.
Heiner, M.: Gilbert, D., Donaldson, R.: Petri Nets for Systems and Synthetic Biology. In: Bernardo, M.; Degano, P.; Zavattaro, G. (eds.): SFM 2008, LNCS 5016, Springer, pp. 215-264, 2008.
Hennessy, M.; Milner, R.: Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM 32 (1985) 1: 137-161.
Hermanns, H.; Herzog, U.; Mertsiotakis, V.: Stochastic Process Algebras - Between LOTOS and Markov chains. Computer Networks and ISDN Systems 30 (1998): 901-924.
Herrmann, P.; Krumm, H.: A Framework for Modeling Transfer Protocols. Computer Networks 34 (2000) 2: 317-337.
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs, 1991.
Holzmann, G.J.: The SPIN Model Checker Primer and Reference Manual. Addi-son-Wesley, Boston, 2004.
Hopcroft, J.E.; Motwani, R.; Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley Longman, Amsterdam, 2007.
ITU-T Recommendation Z.120: Message Sequence Charts (MSC), 1999.
Kröger, F.; Merz, S.: Temporal Logic and State Systems. Springer, 2008.
Lamport, L.: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16 (1994) 3: 872-923.
Manna, Z.; Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, 1992.
Milner, R.: Communication and Concurrency. Prentice Hall. Englewood Cliffs, 1989.
Murata, T.: Petri Nets: Properties, Analysis, and Applications. Proceedings of the IEEE 77 (1989) 4: 541-580.
Conference series of the SDL Forum Society which takes place every two years. It is dedicated to current issues concerning the application and further development of SDL and nowadays of other related language, such as UML, MSC, ASN.1, and TTCN. (see http://www.sdl-forum.org). [Cava 97] and [Dsso 99] are proceedings of this conference series.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
König, H. (2012). 7 Formal description methods. In: Protocol Engineering. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29145-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-29145-6_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29144-9
Online ISBN: 978-3-642-29145-6
eBook Packages: Computer ScienceComputer Science (R0)