ACTLW - an action-based computation tree logic with unless operatorRobert Meolic
, Tatjana Kapus
, Zmago Brezočnik
, 2008, izvirni znanstveni članek
Opis: Model checkers for systems represented by labelled transition systems are not as extensively used as those for systems represented by Kripke structures. This is partially due to the lack of an elegant formal language for property specification which would not be as raw as, for example, HML yet also not as complex as, for example, -calculus. This paper proposes a new action-based propositional branching-time temporal logic ACTLW, which enhances popular computation tree logic (CTL) with the notion of actions in a similar but more comprehensive way than action-based CTL introduced by De Nicola and Vaandrager [R. De Nicola, F.W. Vaandrager, Action versus logics for transition systems, in: Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science, LNCS 469, 1990, pp. 407-419]. ACTLW is defined by using temporal operators until and unless only, whereas all other temporal operators are derived from them. Fixed-point characterisation of the operators together with symbolic algorithms for globalmodel checking are shown. Usage of this new logic is illustrated by an example of verification of mutual-exclusion algorithms.
Ključne besede: formal verification, model checking, action-based temporal logic, fixed point, mutual-exclusion algorithm
Objavljeno: 01.06.2012; Ogledov: 1334; Prenosov: 62
Povezava na celotno besedilo
Representation of Boolean functions with ROBDDsAleš Časar
, Robert Meolic
, samostojni znanstveni sestavek ali poglavje v monografski publikaciji
Opis: This paper describes data structures and algorithms for representation of Boolean functions with reduced ordered binary decision diagrams (ROBDDs). A hash table is used for quick search. Additional information about variables and functions is stored in binary trees. Manipulations on functions are based on a recursive algorithm of ITE operation. The primary goal of this article is describe programming technics needed to realize the idea. For the first time here recursive algorithms for composing functions and garbage collection with a formulae counter are presented. This is better than garbage collection in other known implementations. The results of the tests show that the described representation is very efficient in applications which operate with Boolean functions.
Ključne besede: Reduced Ordered Binary Decision Diagram, Boolean function, logic functions, logic design verification, hash table
Objavljeno: 02.02.2018; Ogledov: 900; Prenosov: 25
Celotno besedilo (323,32 KB)
Applying automated model extraction for simulation and verification of real-life SDL specification with spinBoštjan Vlaovič
, Aleksander Vreže
, Zmago Brezočnik
, 2017, izvirni znanstveni članek
Opis: Formally defined Specification and Description Language (SDL) is used for the design and specification of complex safety-critical systems. Each change in the specification of the product should be immediately checked formally against the requirements’ specification. This paper presents semi-automated system abstraction, automated model extraction, simulation, and formal verification of real-life complex SDL specification. Sound algorithms implemented in our sdl2pml automated model extraction tool preserve all properties of the SDL system. Sdl2pml includes our model of discrete time, abstraction, and support for all relevant SDL functionality and constructs such as dynamic process creation, rational data types, and communication with more than one process instance. To the best of our knowledge, most of them are not supported by any other known approach. We use our SpinRCP tool for simulation and formal verification of the extracted model with the Spin model checker. We demonstrate the applicability of our approach on ISDN User adaptation protocol from SI3000 Softswitch. The extracted Promela model is the largest one ever processed by Spin. We have shown that Spin simulation and model checking can be applied successfully to such huge models.
Ključne besede: formal specifications, automated extraction, formal languages, simulation, formal verification, model cheking, SDL, Promela, SpinRCP, Sdl2pml
Objavljeno: 03.08.2017; Ogledov: 384; Prenosov: 199
Celotno besedilo (13,46 MB)
Gradivo ima več datotek! Več...
E-learning materials for social science studentsMarjan Krašna
, Tomaž Bratina
, 2014, izvirni znanstveni članek
Opis: Today's student population is rightfully categorized as digital natives. From the beginning of their education, they used ICT. The technological gadgets, internet, and social networks are like a glove to them. Such generation of students require more than just textbooks. In the 2013 University of Maribor establish a task force for e-learning materials development. The goal was to identify the optimal technological, didactical and financial approach to the long process of e-learning materials development. Members of the task force have many workshops presenting different views, acquired experiences from their previous projects, technological constraints, prediction, etc. During these workshops it was decided it would be the best to prepare different types of e-learning materials and test them by the students. From their feedbacks we could set the guidelines for large scale production. At the Faculty of Arts, Faculty of Natural Sciences and Mathematics and Faculty of Education students needs to acquire also the digital competences to become successful teachers. For special didactics study programs different types of e-learning materials were produced with different technological approach. The concept was to upgrade the previous deliverables (PowerPoint slides) and narrate them. Narrated slides would enable students to refresh their lectures and should be used as blended e-learning materials. Narrations were prepared in different format: textual narration, voice narration and video narration. But later it was decided that these types are not enough and a mix of narratives (integrated multimedia learning materials) could be used on individual slides depending on the content of the slide. Students first receive the lecture in the classroom and in the same week they need to study associated e-learning materials and write their review of corresponding e-learning materials. In their review students were required to log the required time for studying the e-learning materials; benefits and drawbacks; potential improvement of e-learning materials; and open text of impression of using e-learning materials. Effectiveness and outcomes were tested with the electronic quizzes. Students were highly motivated with these new types of learning materials and provide us valuable feedback. Most efficient were text narrated learning materials, but the favourite was integrated multimedia learning materials. Video and audio narrations take them more time to study since they were constrained with the speed of speech of the recorded lecturer.
Ključne besede: design, distance learning, e-learning, learning materials, validation, verification
Objavljeno: 15.12.2017; Ogledov: 363; Prenosov: 43
Celotno besedilo (1,47 MB)
Gradivo ima več datotek! Več...