Browsing by Subject "formal methods"

Now showing 1 - 5 of 5

Access status: Open Access ,
Concurrent systems modeling with CCL
(Wydawnictwa AGH, 2012) Kułakowski, Konrad
Jednym z podstawowych zadań związanych z inżynierią oprogramowania jest szukanie nowych i optymalizacja istniejących metod modelowania systemów informatycznych. Przedstawiona w pracy notacja CCL stara się wpisywać w ten nurt badań. Prezentowane podejście pokazuje jej użyteczność w kontekście użycia metod strukturalnych (diagramy przepływu danych) do modelowania złożonych systemów informatycznych. Podstawą proponowanej integracji pomiędzy CCL i metodami modelowania strukturalnego jest nowowprowadzone pojęcie eksternalizacji. Pozwala ono abstrahować od szczegółów implementacyjnych komunikacji międzyprocesowej, redukując tym samym wielkość modeli podlegających dalszej weryfikacji. Dzięki przyjętemu rozwiązaniu modele stają się bardziej czytelne dla projektantów, oraz dzięki znaczącej redukcji przestrzeni stanów, możliwe staje się efektywne wykorzystanie metod formalnych w celu ich dalszej analizy.
Access status: Open Access ,
Formalization and analysis of UML 2.0 interaction overview diagram using maude rewriting logic language
(Wydawnictwa AGH, 2024) Djaoui, Chafika; Chaoui, Allaoua
The visual modeling language UML embodies object-oriented design principles. It provides a standard way to visualize the design of a system. It exploits a rich set of well-defined graphical notations for creating abstract models. However, the power of UML is lessened through partially specified formal semantics. Indeed, UML notations are semi-formal and do not lead to fully formalized and executable semantics. Fortunately, UML diagrams are prone to early formalization. Formal methods are a valuable tool that can help overcome the UML constructs’ shortage of firm semantics. It is a powerful way to ascribe precise semantics to the graphical notations used in UML diagrams and models. Our work aims to support the semantics of the UML Interaction Overview Diagram. It introduces an approach to leveraging the strengths of the Maude Rewriting Logic language as a formal specification language. The proposal relies on a model-driven engineering approach. It aims to automate the UML Interaction Overview Diagram’s mapping to a Maude language specification. The Maude language and its linked tools, including the Maude Model Checker, are used to analyze and verify the resulting Maude specification. Finally, an application example shows the feasibility and benefits of the proposed approach.
Access status: Open Access ,
Introduction to modelling embedded systems with Alvis
(Wydawnictwa AGH, 2011) Szpyrka, Marcin; Matyasik, Piotr; Mrówka, Rafał; Witalec, Wojciech; Baniewicz, Jarosław; Kotulski, Leszek
Alvis jest językiem modelowania rozwijanym z myślą o systemach współbieżnych w szczególności systemach wbudowanych. Łączy on w sobie graficzny język modelowania, przeznaczony do definiowania połączeń komunikacyjnych między agentami, z językiem programowania wysokiego poziomu, przeznaczonym do definiowania zachowania poszczególnych agentów. W artykule przedstawiono wybrane aspekty modelowania systemów wbudowanych z użyciem języka Alvis.
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.