Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

The increasing complexity of modern telecommunication systems is one of the main issues encountered in most telecom products. Despite the plethora of methods and tools for efficient system design, verification and validation phases are still consuming significant part of the overall design time. The proposed approach outlines the use of the B method/language for producing correct-by-construction implementations of telecommunication systems. The method described is supported by appropriate tools that automate the process of proving that system properties are maintained during the various design stages. The feasibility of the latter is evaluated in practice through the design of a real world telecom application, borrowed from the domain of wireless telecommunication networks.

REFERENCES

• 1: ATELIER B. 2005. http://www.Atelier_B.societe.com/.
• 2: J.-R. Abrial, The B-book: assigning programs to meanings, Cambridge University Press, New York, NY, 1996
• 3: BOWEN, J. 1996. Specification and Documentation using Z: A Case Study Approach. International Thomson Computer Press.
• 4: DRAPER, J. ET AL. 1996. Evaluating the B-method on an avionics example. In Proceedings of Data Systems in Aerospace (DASIA) Conference, Rome, Italy. European Space Agency Publication Division WPP-116, 89--97.
• 5: ETSI. 2000. Broadband Radio Access Networks BRAN; HIPERLAN Type 2; Data Link Control (DLC) Layer Part1: Basic Data Transport Functions. ETSI TS 101 761-1 v1.1.1.
• 6: Uwe Glässer, Systems Level Specification and Modeling of Reactive Systems: Concepts, Methods, and Tools, Selection of Papers from the Fifth International Workshop on Computer Aided Systems Theory, p.375-385, May 22-25, 1995
• 7: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 8: CORPORATE IEEE, Software engineering standards, IEEE Computer Society Press, Los Alamitos, CA, 1987
• 9: Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 10: KHUN-JUSH J. ET AL. 2002. HIPERLAN Type 2 for Broadband Wireless Communication. Ericsson Review No.2.
• 11: Thomas Kropf, Introduction to Formal Hardware Verification: Methods and Tools for Designing Correct Circuits and Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 12: Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
• 13: George J. Milne, CIRCAL and the representation of communication, concurrency, and time, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.2, p.270-298, April 1985 [doi>10.1145/3318.3322]
• 14: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 15: OMG. 2005. http://www.omg.org/.
• 16: SNOOK, C., TSIOPOULOS, L., AND WALDEN, M. 2003. A Case Study in Requirement Analysis of Control Systems using UML and B. In Proceedings of International Workshop on Refinement of Critical Systems:Methods, Tools and Developments, Turku, Finland.

INDEX TERMS

Keywords:
B language, formal methods, hardware/software codesign, wireless systems