Abstract
A methodology for the description of system requirements and the derivation of formal specifications from system requirements are presented. We will specifically deal with the issues (1) mathematical treatment of system requirements and their relationship with formal specifications represented as state transition systems, (2) a sound and complete system with respect to a system requirement, i.e. a standard system of the system requirement specified as a unique model of the system requirement, (3) derivation of standard systems from system requirements, (4) a support system and an application example, and (5) some comparative discussions on the methodology with partial logical Petri Nets, Production systems, and so on.
Keywords
Download to read the full chapter text
Chapter PDF
References
Chellas, B.F., Modal Logic: An Introduction, Cambridge University Press, 1980.
ISO., Estelle: A Formal Description Technique based on the Extended State Transition Model, ISO 9074, 1989.
ISO., Information Processing Systems - Open System Interconnection - LOTOS - A Formal Description Technique based on the Temporal Ordering of Observational Behavior,IS 8807, 1989.
CCITT., SDL: Specification and Description Language,CCITT Z.100, 1988.
Bolognesi, T., Brinksma, Ed., Introduction to the ISO Specification Language LOTOS, in the Formal Description Technique LOTOS, Elsevier Sci. Pub., pp. 23–73, 1989.
Emerson, E.A., Temporal and Modal Logic, Handbook of Theoretical Computer Science, Elsevier Science Publishers B.V., pp. 995–1072, 1990.
Gotzhein, R., Specifying Communication Services with Temporal Logic, Protocol Specification, Testing and Verification, XL, pp. 295–309, 1990.
van Glabbeek, R.J., The Linear Time - Branching Time Spectrum, Lecture Notes in Comput. Sci. 458, Springer-Verlag, 1990.
Hirakawa, Y., Takenaka, T., Telecommunication Service Description using State Transition Rules, Proc. 6th Int. Work. Software Specification and Design, pp. 140–147, 1991.
Manna, Z., P. Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Trans. on Programming Languages and Systems, 6-, 1, pp. 68–93, 1984.
Milner R., Communication and Concurrency,Prentice-Hall, 1989.
Murata, T., Petri Nets: Properties, Analysis and Applications, IEEE Proc. Vol. 77, No. 4, pp. 541–580, 1989.
Plotkin, G.D., A Structural Approach to Operational Semantics, Computer Science Department, Aarhus University, DAIMI FN-19, 1981.
Shapiro E.Y., Algorithmic Program Debugging, Ph.D. Thesis, The MIT Press, 1982.
Shiratori, N., Sugaware, K., Kinoshita, T., Chakraborty, G., Flexible Networks: Basic Concepts and Architecture, IEICE Trans. Commun., Vol.E77-B, No. 11. pp. 1287–1294, 1994.
Song, K., Togashi, A., Shiratori, N., Verification and refinement for system requirements, IEICE Trans. on Fundamentals of Elec., Comm. and Comput. Sci., Vol. E78-A, No. 11, pp. 1468–1478, 1995.
Togashi, A., Usui, N., Song, K., Shiratori, N. A derivation of System Specifications based on a Partial Logical Petri Net, Proc. of ISCAS95, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Togashi, A., Kanezashi, F., Lu, X. (1997). A Methodology for the Description of System Requirements and the Derivation of Formal Specifications. In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds) Formal Description Techniques and Protocol Specification, Testing and Verification. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35271-8_24
Download citation
DOI: https://doi.org/10.1007/978-0-387-35271-8_24
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5260-1
Online ISBN: 978-0-387-35271-8
eBook Packages: Springer Book Archive