In this article, we introduce a probabilistic verification algorithm for stochastic regular expressions over a probabilistic extension of the Action based Computation Tree Logic (ACTL*). The main results include a novel model checking algorithm and a semantics on the probabilistic action logic for stochastic regular expressions (SREs). Specific to our model checking algorithm is that SREs are defined via local probabilistic functions. Such functions are beneficial since they enable to verify properties locally for sub-components. This ability provides a flexibility to reuse the local results for the global verification of the system; hence, the framework can be used for iterative verification. We demonstrate how to model a system with an SRE and how to verify it with the probabilistic action based logic and present a preliminary performance evaluation with respect to the execution time of the reachability algorithm.
W artykule przeprowadzono rozważania nt. współczesnego, praktycznego znaczenia podstawowych modeli formalnych z dziedziny ochrony informacji. Przedstawiono także Podstawowe Twierdzenie Bezpieczeństwa (ang. Basic Security Theorem) oraz pokazano przykład jego uściślenia na bazie modelu Bella-LaPaduli.
EN
The paper considers the contemporary practical importance of basic formal models within the area of information security. The Basic Security Theorem is presented and an example of its reference to the Bell-LaPadula model is given.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.