Browsing by Subject "verification"

Now showing 1 - 5 of 5

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 ,
Type-driven development of concurrent communicating systems
(Wydawnictwa AGH, 2017) Brady, Edwin
Modern software systems rely on communication, for example mobile applcations communicating with a central server, distributed systems coordinaing a telecommunications network, or concurrent systems handling events and processes in a desktop application. However, reasoning about concurrent prgrams is hard, since we must reason about each process and the order in which communication might happen between processes. In this paper, I describe a type-driven approach to implementing communicating concurrent programs, using the dependently typed programming language Idris. I show how the type system can be used to describe resource access protocols (such as controlling access to a file handle) and verify that programs correctly follow those prtools. Finally, I show how to use the type system to reason about the order of communication between concurrent processes, ensuring that each end of a communication channel follows a defined protocol.
Access status: Open Access ,
Verification mechanism for lightweight component-based environment based on IoC container
(Wydawnictwa AGH, 2013) Leszko, Rafał; Piętak, Kamil
This paper presents a concept of component verification framework dedicated to a particular lightweight component environment. The starting point of the paper constitutes a discussion about the significance of verification of syntax inconsistencies in software development. Next, the need of verification in service-oriented and component-based systems is presented, and various approaches of verification in existing component environments are explained. The main part of the paper introduces a concept of functional integrity of component-based systems that utilize verification mechanisms which check consistency between components. The proposed solution is built on a fine-grained component environment (close to classes similarly to the Spring Framework) realized in the AgE platform. Selected technical aspects of framework design illustrate the considerations of the paper.
Access status: Restricted ,
Weryfikacja i porównanie osuwisk zaistniałych na terenie gmin Lubień i Dobczyce
(Data obrony: 2016-10-18) Drabik, Łukasz
Wydział Geologii, Geofizyki i Ochrony Środowiska
W niniejszej pracy dyplomowej zostały zaprezentowane wyniki badań przeprowadzonych na osuwiskach w znajdujących się na terenie gmin Lubień i Dobczyce. Przed rozpoczęciem badań przeanalizowano materiały archiwalne, a w szczególności System Osłony Przeciwosuwiskowej. Badania objęły pomiar parametrów geometrycznych osuwiska (długość, szerokość, wysokość skarpy głównej itd.), ocenę warunków geomorfologicznych i geologicznych, określenie typu osuwisk oraz rodzaju podłoża gruntowego. Inwentaryzację osuwisk przeprowadzono jesienią 2014r. oraz wiosną 2015r. Na końcu porównano osuwiska występujące w obu gminach pod względem badanych parametrów.
Access status: Open Access ,
Weryfikacja procesów biznesowych metodą tablic semantycznych
(Wydawnictwa AGH, 2010) Klimek, Radosław; Skrzyński, Paweł; Turek, Michał
This paper describes the results of work on stabilizing the methodology for formal correctness verification of processes recorded in a process model with BPMN notation. The main path of a solution is to carry out the conversion of BPMN model to set of specially designed logic formulas. Afterwards - to formal verify the correctness of formulas using the calculation provided by the authors. A semantic table method has been applied in the verification process. The approach could provide interesting alternative to the traditional approach, allowing relatively easy errors identification in the specification process.