Formalna analiza interpretowanych algorytmicznych maszyn stanów ASM z wykorzystaniem narzędzia model checker

Algorithmic state machines ASM are one of formal methods of embedded systems specification. They are defined during system project phase. Potential not detected errors in specification may generate unnecessary costs, and in case of dependable systems they may even have catastrophic causes. The article presents formal verification and analysis method of algorithmic state machines using computer deduction in temporal logic (Model Checking technique). Model checker tools enable automatic verification of system specification by checking consistency between model description and requirements which have to be satisfied in the model. The paper concentrates on NuSMV model checker. Formal verification technique Model Checking is discussed basing on presented case study.