@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00118729, book = {全国大会講演論文集}, issue = {ソフトウェア工学}, month = {Mar}, note = {システム開発において、その仕様を形式的に記述することにより、実現されたシステムと仕様の間に論理的矛盾がないかどうかを検証することができる。我々は、このような検証をオートマトンを用いて機械的に行うシステムATVS(Automated Testing and Verification System)を開発している。ATVSで対象としている仕様はシステムの設計仕様であり、それは有限状態機械(Finite State Machine 以下、FSMと略す)により表現される。しかし、実際の製品仕様をFSMで記述しようとすると、記述性や理解性の点で問題がある。また、ATVSの検証能力自体も改良の余地がある。本稿では、まずATVSにおける検証の概要について述べ、次に仕様記述の拡張と検証機能の追加、その実現に伴うATVSの拡張について述べる。なお、このATVSは一貫ソフト開発支援システムIMAPの一環として開発している。}, pages = {1027--1028}, publisher = {情報処理学会}, title = {自動検証システムATVSの拡張}, volume = {第40回}, year = {1990} }