問題タブ [formal-methods]

これは、予定 DB の Z スキーマです。

の名前に基づいて予定を見つける検索機能を作成したいと思いますattendees。

1. 検索機能が予定オブジェクトのすべての詳細を返すようにします。

どのように設計すればよいですか？

これが私の見解です：

Isabelle/HOL 証明アシスタントには、Coq と比較して弱点と長所がありますか?

私は正式な方法論の分野には不慣れですが、その応用について十分な知識を持っていると感じています。しかし、私はソフトウェアが作成されるときに、開発プロセスに適用される形式的な方法にしか遭遇しないようです。

既存のソフトウェアに正式な方法を適用して、役割ベースのアクセス制御 (RBAC) と、 Bell-LaPadula (BLP) 方法に従った機密情報の分離に準拠しているかどうかをテストできるようにしたいと考えています。

既存のソフトウェア/ソース コードの RBAC および BLP のような検証のための自動化されたソリューションを提供する、どのような方法とツールを知っていますか?

乾杯、

M.フォロズ

ispin でシステムをモデル化しましたが、LTL 式を使用してシステムを検証しようとすると、次のような到達不能エラーが見つかりました

私のLTL式は

リストがあるとします：

変更可能なリストについて話していることに注意してください。そして、自明な再帰的な長さ関数:

当然、リストが非循環の場合にのみ終了します。

この述語は、再帰関数として実装されているため、循環リストで終了しないことに注意してください。

通常、リストの長さを有界の減少要因として使用するリスト トラバーサル終了の証拠を目にします。Length彼らはそれが非負であると考えています。しかし、私が見る限り、この事実 ( ) はそもそもLength l >= 0の終了から導かれます。Length

が終了し、 （または同等の、より適切に定義された述語）リストでLength非負であることをどのように証明しますか?NonCircular

ここで重要な概念が欠けていますか?

プロセス a またはプロセス b がクリティカル セクションに入りますが、同時にではありません。これが発生した場合 (つまり、それらが同時にクリティカル セクションに入った場合)、割り込みが実行されます。

p = プロセス a

q = プロセス b

r = クリティカル セクション

演算子 ∨ = または

演算子 → = 含意

私の答え ：

(p ∨ q) → r

これは正しいですか、それとも私が何か間違ったことをしましたか? 命題論理を理解しようとしています。