Abstract
When developing hard- or software systems one starts with a collection of requirements. Most requirements arise due to the needs of the customer, others originate from design decisions and further constraints. Of course, the final system should fulfill these requirements. Besides general requirements like scalability and performance, there is often a large number of formal requirements which concern the functionality of the system. Typical requirements of this kind are lifeness requirements (e.g. bad things never happen), fairness requirements (e.g. the system continues doing meaningful things), and in general requirements which prescribe the chronological order of events (e.g. event A may only occur after event B).
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 subscriptionsPreview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Berg, T., Raffelt, H. (2005). 19 Model Checking. In: Broy, M., Jonsson, B., Katoen, JP., Leucker, M., Pretschner, A. (eds) Model-Based Testing of Reactive Systems. Lecture Notes in Computer Science, vol 3472. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11498490_25
Download citation
DOI: https://doi.org/10.1007/11498490_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26278-7
Online ISBN: 978-3-540-32037-1
eBook Packages: Computer ScienceComputer Science (R0)