Browsing by Subject "model checking"

Now showing 1 - 5 of 5

Access status: Open Access ,
Code generation for CSM/ECSM models in COSMA environment
(2007) Grabski, Waldemar; Nowacki, Michał
The COSMA software environment, developed in the Institute of Computer Science, WUT, was designed primarily for model checking of reactive systems specified in terms of Concurrent State Machines (CSM). However, COSMA supports also Extended CSM (ECSM). The extensions allow for using complex data types and pieces of C/C++ code, attributed to CSM states and/or transitions. Because of these extensions, ECSM models cannot be verifed by model checking, but they can be used as an intermediate step in code generation. The underlying CSM represent then the flow of control within cooperating components and the communication among them while the extensions specify the data structures and the details of their processing. The paper discusses the code generation from ECSM diagrams. The approach is illustrated with an example.
Access status: Open Access ,
Formal analysis of use case diagrams
(Wydawnictwa AGH, 2010) Klimek, Radosław; Szwed, Piotr
Use case diagrams play an important role in modeling with UML. Careful modeling is crucial in obtaining a correct and efficient system architecture. The paper refers to the formal analysis of the use case diagrams. A formal model of use cases is proposed and its construction for typical relationships between use cases is described. Two methods of formal analysis and verification are presented. The first one based on a states' exploration represents a model checking approach. The second one refers to the symbolic reasoning using formal methods of temporal logic. Simple but representative example of the use case scenario verification is discussed.
Access status: Open Access ,
Model checking processes specified in join-calculus algebra
(Wydawnictwa AGH, 2014) Maludziński, Sławomir P.; Dobrowolski, Grzegorz
This article presents a model checking tool used to verify concurrent systems specified in join-calculus algebra. The temporal properties of systems under verification are expressed in CTL logic. Join-calculus algebra, with its operational semantics defined by a chemical abstract machine, serves as the basic method for the specification of concurrent systems and their synchronization mechanisms, allowing for the examination of more complex systems. The described model checker is a proof of concept for the utilization of new methodologies of formal system specification and verification in software engineering practice.
Access status: Open Access ,
Timed concurrent state machines
(2007) Daszczuk, Wiktor Bohdan
Timed Concurrent State Machines are an application of Alur Timed Automata concept to coincidence-based (rather than interleaving) CSM modeling technique. TCSM support the idea of testing automata, allowing to specify time properties easier than temporal formulas. Also, calculation of a global state space in real-time domain (Region Concurrent State Machines) is defined, allowing to storę a verified system in ready-to-verification form, and to multiply it by various testing automata.
Access status: Open Access ,
Using splitter ordering heuristics to improve bisimulation in probabilistic model checking
(Wydawnictwa AGH, 2025) Mohagheghi, Mohammadsadegh; Salehi, Khayyam
Model checking is used to verify computer-based and cyber-physical systems, but faces challenges due to state space explosion. Bisimulation minimization reduces states in transition systems, easing this issue. Probabilistic bisimulation further simplifies models with stochastic behaviors. Recent techniques aim to improve the time complexity of iterative methods in computing probabilistic bisimulation for stochastic systems with nondeterministic behaviors. In this paper, we propose several techniques to accelerate iterative processes to partition the state space of a given probabilistic model to its bisimulation classes. The first technique applies two ordering heuristics for choosing splitter blocks. The second technique uses hash tables to reduce the running time and the average time complexity of the standard iterative method. The proposed approaches are implemented and run on several conventional case studies and reduce the running time by one order of magnitude on average.