Использование метода покрытий при верификации моделей IDEF-0
Аннотация
Разработка программного обеспечения с использованием моделирования зачастую сталкивается с проблемами ресурсоемкости проверки моделей комплексных систем. Данная статья рассматривает метрические показатели симуляционного тестирования и их применение в контексте непосредственной верификации моделей.Литература
Подъячев А. Ю., Афанасьев С. В. Тестирование трансляции формальных моделей // Тру- ды СПИИРАН. СПб.: Наука, 2006. Вып. 3, т. 2. C.156–161.
Budd T. A., Angluin D. Two notions of correctness and their relation to testing // Acta Informatica. 1992, issue 18. P. 31–45.
Armon R., Fix L., Flaisher A., Grumberg O., Piterman N., Vardi M. Y. Enhanced vacuity detection for linear temporal logic in Computer Aided Verification // Proc. 15th International Conference. Springer-Verlag, 2003.
Beatty D., Bryant R. Formally verifying a microprocessor using a simulation methodology // Proc. 31st Design Automation Conference. IEEE Computer Society, 1994. P. 596–602.
Bening L., Foster H. Principles of verifiable RTL design – a functional coding style supporting verification processes. Kluwer Academic Publishers, 2000.
Clarke E. M., Grumberg O., Peled D. Model Checking. MIT Press, 1999.
Chockler H., Kupferman O., Yardi M. Y. Coverage Metrics for Formal Verification, Jerusalem, 2003.
Peled D. Software Reliability Methods. Springer-Verlag, 2001.
Born M., Schieferdecker I., Li M. UML Framework for Automated Generation of Component-Based Test Systems. Software Engineering Applied to Networking and Parallel // Distributed Computing, Reims, France, 2000.
Budd T. A., Angluin D. Two notions of correctness and their relation to testing // Acta Informatica. 1992, issue 18. P. 31–45.
Armon R., Fix L., Flaisher A., Grumberg O., Piterman N., Vardi M. Y. Enhanced vacuity detection for linear temporal logic in Computer Aided Verification // Proc. 15th International Conference. Springer-Verlag, 2003.
Beatty D., Bryant R. Formally verifying a microprocessor using a simulation methodology // Proc. 31st Design Automation Conference. IEEE Computer Society, 1994. P. 596–602.
Bening L., Foster H. Principles of verifiable RTL design – a functional coding style supporting verification processes. Kluwer Academic Publishers, 2000.
Clarke E. M., Grumberg O., Peled D. Model Checking. MIT Press, 1999.
Chockler H., Kupferman O., Yardi M. Y. Coverage Metrics for Formal Verification, Jerusalem, 2003.
Peled D. Software Reliability Methods. Springer-Verlag, 2001.
Born M., Schieferdecker I., Li M. UML Framework for Automated Generation of Component-Based Test Systems. Software Engineering Applied to Networking and Parallel // Distributed Computing, Reims, France, 2000.
Опубликован
2007-10-01
Как цитировать
Подъячев,. (2007). Использование метода покрытий при верификации моделей IDEF-0. Труды СПИИРАН, (5), 275-283. https://doi.org/10.15622/sp.5.17
Выпуск
Раздел
Статьи
Авторы, которые публикуются в данном журнале, соглашаются со следующими условиями:
Авторы сохраняют за собой авторские права на работу и передают журналу право первой публикации вместе с работой, одновременно лицензируя ее на условиях Creative Commons Attribution License, которая позволяет другим распространять данную работу с обязательным указанием авторства данной работы и ссылкой на оригинальную публикацию в этом журнале.
Авторы сохраняют право заключать отдельные, дополнительные контрактные соглашения на неэксклюзивное распространение версии работы, опубликованной этим журналом (например, разместить ее в университетском хранилище или опубликовать ее в книге), со ссылкой на оригинальную публикацию в этом журнале.
Авторам разрешается размещать их работу в сети Интернет (например, в университетском хранилище или на их персональном веб-сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению, а также к большему количеству ссылок на данную опубликованную работу (Смотри The Effect of Open Access).
