Overview SyncStitch is a model checker based on the process algebra CSP (Communicating Sequential Processes). By using SyncStitch, you can check six types of properties of the system you are developping: Deadlocks Divergences (also known as livelocks) Refinement relation on traces semantics (safety) Refinement relation on stable failures semantics (safety and liveness) LTL (Linear-Time Logic) with
証明支援系Globularを使っている人っているのかな？ まー、いても少数でしょうね。僕はたまに使います。しばらく使わないでいると使い方を忘れます。少なくとも一人のユーザー（＝僕・檜山）にとっては意味があるので、「Globularの使い方」を記録しておきます。 何回かに分けますが、気が向いたら書くつもりなので全体で何回になるか分かりません。何をどこまで書くかの計画もありません。 内容： はじめに 参考URL ワークスペースの管理など 画面構成 左側がセルパレット 中央がビューペイン ビューコントロールとビューイング方式 シリーズ目次 Globularの使い方 (1) Globularの使い方 (2)： サンプル・ワークスペース Globularの使い方 (3)： 定理と証明 はじめに Globularは、機能的には“ある種の”お絵描きソフトです。普通のお絵描きソフトと違うのは、n次元（n
形式手法（Bメソッド） 形式手法とは 形式手法は、数学を基盤としたソフトウエアやシステムの仕様記述、検証、開発手法の総称で、数多くの手法が考案されています。 形式仕様記述を用いて厳密に仕様を定義することによる仕様の曖昧性の排除・仕様の前提条件の明確化や、形式検証での数学的解析による開発ソフトウェアの信頼性・頑健性の向上が可能となります。 形式手法の分類 ・形式仕様記述 - モデル規範…集合論・述語論理を用いて仕様を表現 - 性質規範…代数仕様を用いて仕様を表現 ・形式検証 - 定理証明…要求・仕様と設計や実装との間の論理的整合性や一貫性処理の正しさを数学的に証明する - モデル検査…振る舞いについて全状態空間を時相論理式などを用いて自動検査 ・形式プログラム合成 形式手法の分類 機能安全規格IEC 61508や情報セキュリティ評価の為のコモンクライテリアISO/IEC15408といった安全
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
