Formal Methods

At RISC we understand by formal methods the application of methods from symbolic computation (especially from formal logic) to rigorously reason about properties of computer programs, in particular to verify their correctness with respect to a specification.

The term "formal methods" applies to all techniques that make computer software and computing systems subject to formal reasoning. By treating a computer program as a mathematical object with a formal semantics, we can rigorously argue about its behavior, e.g., why it always computes the correct result; this reasoning can be supported or even automated by corresponding software. Formal methods are industrially applied wherever computer/program failures are not acceptable, e.g. to mission-critical software, computer chips, or communication protocols.

Formal methods comprise at least two aspects:

  1. "Specification" means to describe the expected behavior of a program in a mathematically precise way (e.g. as a logic formula, see the "ensures" clause in the attached picture which gives the specification of a program).
  2. "Verification": means to demonstrate with mathematical rigor that every possible execution of the program does not crash and indeed satisfies its specification, preferably with computer support (by reasoners that apply proof-based techniques or by model checkers that investigate the space of all possible executions).

Furthermore, the "Validation" of a specification aims to ensure that this specification actually describes the intended behavior; thus the verification of a program with respect to this specification indeed demonstrates that the program satisfies the properties that we are interested in.

Even if the complete verification of a program may sometimes not be feasible, a "light-weight" application of formal methods may help to increase our confidence in the correctness of a program:

  • "Extended Static Checking" and "Bounded Model Checking" apply logic-based techniques to detect errors in a program; while these techniques do not necessarily ensure that a program is correct (they falsify a program rather than verifying it), they at least raise its quality;
  • "Runtime Verification" supervises the execution of a program by an automatically generated monitor that triggers a warning if the program violates its specification; while this does not rule out possible future errors, it at least ensures that the execution so far has been correct.

The support respectively automation of all these aspects by software (automated program verifiers, interactive verification assistants, model checkers, static program analyzers, specification analyzers) is a hot topic of research.

Software

RISC ProgramExplorer

An Interactive Program Reasoning Environment

The RISC ProgramExplorer is a computer-supported program reasoning environment for a simple imperative programming language "MiniJava"; it incorporates the RISC ProofNavigator as a semi-automatic proving assistant. The environment has been developed mainly for educational purposes (see this paper for a ...

MoreSoftware Website

RISC ProofNavigator

An Interactive Proof Assistant for Program/System Verification

The RISC ProofNavigator is an interactive proof assistant for supporting formal reasoning about computer programs and computing systems, see the README file and this short paper for the main ideas; it is the core reasoning component of the RISC ProgramExplorer. ...

MoreSoftware Website

RISCAL

The RISC Algorithm Language: A Language and Associated Software System for Specifying and Verifying Mathematical Algorithms

The RISC Algorithm Language (RISCAL) is a specification language and associated software system for describing mathematical algorithms, formally specifying their behavior based on mathematical theories, and validating the correctness of algorithms, specifications, and theories by execution/evaluation. The software has been ...

MoreSoftware Website

Publications

2018

Idempotent Anti-unification

David M. Cerna Temur Kutsia

RISC. Technical report, Feb. 2018. Submitted for review. [pdf]
[bib]
@techreport{RISC5530,
author = {David M. Cerna Temur Kutsia},
title = {{Idempotent Anti-unification }},
language = {english},
abstract = {In this paper we address two problems related to idempotent anti-unification. First, we show thatthere exists an anti-unification problem with a single idempotent symbol which has an infiniteminimal complete set of generalizations. It means that anti-unification with a single idempotentsymbol has infinitary or nullary generalization type, similar to anti-unification with two idem-potent symbols, shown earlier by Loı̈c Pottier. Next, we develop an algorithm, which takes anarbitrary idempotent anti-unification problem and computes a representation of its solution set inthe form of a regular tree grammar. The algorithm does not depend on the number of idempotentfunction symbols in the input terms. The language generated by the grammar is the minimalcomplete set of generalizations of the given anti-unification problem, which implies that idem-potent anti-unification is infinitary.},
year = {2018},
month = {Feb.},
note = {Submitted for review},
institution = {RISC},
length = {27}
}

Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models

Wolfgang Schreiner, Alexander Brunhuemer, Christoph Fürst

In: Post-Proceedings ThEdu'17, Pedro Quaresma and Walther Neuper (ed.), Proceedings of 6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg, Sweden, 6 Aug 2017, Electronic Proceedings in Theoretical Computer Science (EPTCS) 267, pp. 120-139. 2018. Open Publishing Association, ISSN 2075-2180. [url] [pdf]
[bib]
@inproceedings{RISC5531,
author = {Wolfgang Schreiner and Alexander Brunhuemer and Christoph Fürst},
title = {{Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models}},
booktitle = {{Post-Proceedings ThEdu'17}},
language = {english},
abstract = {Education in the practical applications of logic and proving such as the formalspecification and verification of computer programs is substantially hampered bythe fact that most time and effort that is invested in proving is actuallywasted in vain: because of errors in the specifications respectively algorithmsthat students have developed, their proof attempts are often pointless (becausethe proposition proved is actually not of interest) or a priori doomed to fail(because the proposition to be proved does actually not hold); this is afrequent source of frustration and gives formal methods a bad reputation. RISCAL(RISC Algorithm Language) is a formal specification language and associatedsoftware system that attempts to overcome this problem by making logicformalization fun rather than a burden. To this end, RISCAL allows students toeasily validate the correctness of instances of propositions respectivelyalgorithms by automatically evaluating/executing and checking them on (small)finite models. Thus many/most errors can be quickly detected and subsequentproof attempts can be focused on propositions that are more/most likely to beboth meaningful and true.},
series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
volume = {267},
pages = {120--139},
publisher = {Open Publishing Association},
isbn_issn = {ISSN 2075-2180},
year = {2018},
editor = {Pedro Quaresma and Walther Neuper},
refereed = {yes},
keywords = {formal methods, program specification and verification, model checking, computer science education, logic},
sponsor = {Supported by the Johannes Kepler University Linz, Linz Institute of Technology (LIT), Project LOGTECHEDU "Logic Technology for Computer Science Education"},
length = {20},
conferencename = {6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg, Sweden, 6 Aug 2017},
url = {http://dx.doi.org/10.4204/EPTCS.267.8}
}

Idempotent Generalization is Infinitary

David M. Cerna and Temur Kutsia

RISC. Technical report, RISC Report, 2018. [pdf]
[bib]
@techreport{RISC5529,
author = {David M. Cerna and Temur Kutsia},
title = {{Idempotent Generalization is Infinitary}},
language = {english},
abstract = {Let §\mathbf{I}_{S}$ be an equational theory s.t. for each $f\in S$, $f(x,x)=x$. Such an equational theory is said to be {\em idempotent}. It is known that the anti-unification problem (AUP) $f(a,b) \triangleq g(a,b)$ modulo $\mathbf{I}_{\lbrace f,g \rbrace}$ admits infinitely many least-general generalizers (lggs)~\cite{LPottier1989}. We show that, modulo $\mathbf{I}_{\lbrace f\rbrace}$, $f(a,f(a,b)) \triangleq f(b,f(a,b))$ admits infinitely many lggs.},
year = {2018},
howpublished = {RISC Report},
institution = {RISC},
length = {1}
}

WebEx: Web Exercises for RISCAL

Wolfgang Schreiner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, October 2018. [pdf]
[bib]
@techreport{RISC5793,
author = {Wolfgang Schreiner},
title = {{WebEx: Web Exercises for RISCAL}},
language = {english},
abstract = {We report on a software framework "WebEx" for developing web-basedstudent exercises whose correctness is checked with the help of the RISCAL (RISCAlgorithm Language) software. This framework allows to generate from anappropriately annotated RISCAL specification file an HTML file that serves asthe frontend to a remote execution service. Student input (RISCAL fragments) aretransmitted to this execution service which generates from the annotatedspecification file and the input a plain RISCAL specification on which RISCAL isinvoked (in a non-interactive mode); the success status of the execution and theproduced output are reported back to the web interface. For each successfulexercise the server produces a digitally signed certificate that is returned tothe user who may submit this certificate as a proof of successful completion ofthe exercise (which may be subsequently automatically checked). Furthermore eachannotated RISCAL specification may serve as a template that may be instantiatedwith other data to produce a set of exercise instances. The WebEx software ismostly independent of RISCAL; it may be also used to provide a web front end forother scientific software of a similar nature.},
year = {2018},
month = {October},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, logic, computer-supported education},
sponsor = {Austrian OEAD WTZ program and the Slovak SRDA agency contract SK 14/2018 SemTech and Johannes Kepler University Linz, Linz Institute of Technology (LIT), Project LOGTECHEDU},
length = {35}
}

On the Probabilistic Model Checking of Cognitive Radio Networks and Cognitive Infocommunication Systems

Wolfgang Schreiner, Tamás Bérczes, János Sztrik, Hamza Nemouchi

Technical report no. 18-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. February 2018. [pdf]
[bib]
@techreport{RISC5595,
author = {Wolfgang Schreiner and Tamás Bérczes and János Sztrik and Hamza Nemouchi},
title = {{On the Probabilistic Model Checking of Cognitive Radio Networks and Cognitive Infocommunication Systems}},
language = {english},
abstract = {We report on the usage of the probabilistic model checker PRISM to validate respectively falsify previouslypublished results on the performance of cognitive radio networks and other cognitive infocommunicationsystems. For this purpose, we construct formal system models in the PRISM modeling languageas Continuous Time Markov Chains (CTMCs) that are analyzed with the help of queries formulated in avariant of continuous stochastic logic (CSL). It is shown that many results can be accurately reproduced butalso that a few previously reported results are clearly erroneous. Furthermore, we report several deviationsfrom previously reported results where the reasons are unclear and need further investigation. Here a majorproblem is that the systems that have been analyzed in literature are usually just described in informallanguage which leaves ample room for interpretation. This makes the reconstruction of corresponding formalsystem models and the reproduction of performance measures a difficult task and limits the long-termscientific value of the reported results.},
number = {18-04},
year = {2018},
month = {February},
keywords = {formal methods, performance analysis, queueing systems},
sponsor = {Supported by the Stiftung Aktion Österreich-Ungarn project 96öu8 “Engineering Information Technology Modelling and Design of Cognitive Radio Networks”},
length = {24},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Visualizing Execution Traces in RISCAL

Wolfgang Schreiner, William Steingartner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, March 2018. [pdf]
[bib]
@techreport{RISC5610,
author = {Wolfgang Schreiner and William Steingartner},
title = {{Visualizing Execution Traces in RISCAL}},
language = {english},
abstract = {We report on initial results concerning the visualization of execution traces ofalgorithms that are formally specified and modeled in the RISC AlgorithmLanguage (RISCAL); these algorithms are executed and visualized in theassociated software system which also validates their correctness by checkingthe satisfaction of the formal contracts. This work has been stimulated bycorresponding visualization of Jane, a language with an associated toolkit that has been developed to demonstrate the categorical semantics ofprogramming languages. By the new visualization extension of RISCAL, thesuitability of the software for the purpose of computer science education shallbe improved.},
year = {2018},
month = {March},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, verification, model checking},
sponsor = {Austrian OEAD WTZ and Slovak SRDA contract SK 14/2018 "SemTech", JKU Linz Institute of Technology (LIT) project "LOGTECHEDU"},
length = {7}
}

Validating Mathematical Theories and Algorithms with RISCAL

Wolfgang Schreiner

In: Intelligent Computer Mathematics, F. Rabe, W. Farmer, G. Passmore, A. Youssef (ed.), Proceedings of CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 13-17, 2018, Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence 11006, pp. 248-254. 2018. Springer, Berlin, ISBN 978-3-319-96811-7. The final authenticated version is available online at Springer. [url] [pdf]
[bib]
@inproceedings{RISC5704,
author = {Wolfgang Schreiner},
title = {{Validating Mathematical Theories and Algorithms with RISCAL}},
booktitle = {{Intelligent Computer Mathematics}},
language = {english},
abstract = {RISCAL is a language for describing mathematical algo-rithms and formally specifying their behavior with respect to user-definedtheories in first-order logic. This language is based on a type system thatconstrains the size of all types by formal parameters; thus a RISCALspecification denotes an infinite class of models of which every instancehas finite size. This allows the RISCAL software to fully automaticallycheck in small instances the validity of theorems and the correctness ofalgorithms. Our goal is to quickly detect errors respectively inadequa-cies in the formalization by falsification in small model instances beforeattempting actual correctness proofs for the whole model class.},
series = {Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence},
volume = {11006},
pages = {248--254},
publisher = {Springer},
address = {Berlin},
isbn_issn = {ISBN 978-3-319-96811-7},
year = {2018},
note = {The final authenticated version is available online at Springer},
editor = {F. Rabe and W. Farmer and G. Passmore and A. Youssef},
refereed = {yes},
keywords = {Formal specification, Falsification, Model checking},
sponsor = {Supported by the Johannes Kepler University, Linz Institute of Technology (LIT), project LOGTECHEDU, and by the OEAD WTZ project SK 14/2018 SemTech.},
length = {7},
conferencename = {CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 13-17, 2018},
url = {https://doi.org/10.1007/978-3-319-96812-4_21}
}

Logic as a Path to Enlightenment (Work in Progress Report)

Wolfgang Schreiner

In: Computer Mathematics in Education - Enlightenment or Incantation?, Walther Neuper (ed.), Proceedings of CME-EI18, Workshop at CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 17, 2018., pp. 1-5. August 2018. To be published at CEUR Workshop Proceedings, http://CEUR-ws.org, ISSN 1613-0073. [pdf]
[bib]
@inproceedings{RISC5711,
author = {Wolfgang Schreiner},
title = {{Logic as a Path to Enlightenment (Work in Progress Report)}},
booktitle = {{Computer Mathematics in Education - Enlightenment or Incantation?}},
language = {english},
pages = {1--5},
publisher = {To be published at CEUR Workshop Proceedings, http://CEUR-ws.org},
isbn_issn = {ISSN 1613-0073},
year = {2018},
month = {August},
editor = {Walther Neuper},
refereed = {yes},
keywords = {RISC Algorithm Language, RISCAL, Model Checking, Verification},
sponsor = {Supported by the Johannes Kepler University, Linz Institute of Technology (LIT), project LOGTECHEDU, and by the OEAD WTZ project SK 14/2018 SemTech.},
length = {3},
conferencename = {CME-EI18, Workshop at CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 17, 2018.}
}

Visualizing Logic Formula Evaluation in RISCAL

Wolfgang Schreiner, William Steingartner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, July 2018. [pdf]
[bib]
@techreport{RISC5721,
author = {Wolfgang Schreiner and William Steingartner},
title = {{Visualizing Logic Formula Evaluation in RISCAL}},
language = {english},
abstract = {We report on initial results concerning the visualization of the evaluation oflogic formulas that are formulated in the RISC Algorithm Language (RISCAL). Suchformulas usually represent propositions that are supposed to be true; examplesare mathematical theorems or verification conditions of algorithms that havebeen formally modeled and specified in RISCAL. The visualization is intended toaid the user to understand the truth value of a formula, in particular in thosecases where a formula is unexpectedly not valid. To this aim, the visualizationof a formula consists of a pruned evaluation tree that depicts exactly thoseevaluation branches that contribute to the overall truth value.},
year = {2018},
month = {July},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
keywords = {formal methods, verification, model checking},
sponsor = {Supported by the Johannes Kepler University, Linz Institute of Technology (LIT), project LOGTECHEDU, and by the OEAD WTZ project SK 14/2018 SemTech.},
length = {13}
}

2017

Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications

David M. Cerna , Wolfgang Schreiner

In: Epic series in computer science, Mohamed Mosbah, Michaël Rusinowitch (eds). (ed.), Proceedings of SCSS 2017, 8th International Symposium on Symbolic Computation in Software Science, Epic 45, pp. 1-15. April 2017. Easy chair, ISSN 2398-7340. [url] [pdf]
[bib]
@inproceedings{RISC5404,
author = {David M. Cerna and Wolfgang Schreiner},
title = {{Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications}},
booktitle = {{Epic series in computer science}},
language = {english},
abstract = {Measuring the Gap: Algorithmic Approximation Bounds for the Space Complexity of Stream Specifications},
series = {Epic},
volume = {45},
pages = {1--15},
publisher = {Easy chair},
isbn_issn = {ISSN 2398-7340},
year = {2017},
month = {April},
editor = {Mohamed Mosbah and Michaël Rusinowitch (eds).},
refereed = {yes},
length = {12},
conferencename = {SCSS 2017, 8th International Symposium on Symbolic Computation in Software Science},
url = {http://easychair.org/publications/download/Measuring_the_Gap_Algorithmic_Approximation_Bounds_for_the_Space_Complexity_of_Stream_Specifications}
}

Ceres in Intuitionistic Logic

David Cerna, Alexander Leitsch, Giselle Reis, Simon Wolfsteiner

Annals of Pure and Applied Logic, pp. 1783-1836. October 2017. Elsevier, ISSN 0168-0072. [url]
[bib]
@article{RISC5429,
author = {David Cerna and Alexander Leitsch and Giselle Reis and Simon Wolfsteiner},
title = {{Ceres in Intuitionistic Logic}},
language = {english},
abstract = {Abstract In this paper we present a procedure allowing the extension of a CERES-based cut-elimination method to intuitionistic logic. Previous results concerning this problem manage to capture fragments of intuitionistic logic, but in many essential cases structural constraints were violated during normal form construction resulting in a classical proof. The heart of the \{CERES\} method is the resolution calculus, which ignores the structural constraints of the well known intuitionistic sequent calculi. We propose, as a method of avoiding the structural violations, the generalization of resolution from the resolving of clauses to the resolving of cut-free proofs, in other words, what we call proof resolution. The result of proof resolution is a cut-free proof rather than a clause. Note that resolution on ground clauses is essentially atomic cut, thus using proof resolution to construct cut-free proofs one would need to join the two proofs together and remove the atoms which where resolved. To efficiently perform this joining (and guarantee that the resulting cut-free proof is intuitionistic) we develop the concept of proof subsumption (similar to clause subsumption) and indexed resolution, a refinement indexing atoms by their corresponding positions in the cut formula. Proof subsumption serves as a tool to prove the completeness of the new method CERES-i, and indexed resolution provides an efficient strategy for the joining of two proofs which is in general a nondeterministic search. Such a refinement is essential for any attempt to implement this method. Finally we compare the complexity of CERES-i with that of Gentzen-based methods.},
journal = {Annals of Pure and Applied Logic},
pages = {1783--1836},
publisher = {Elsevier},
isbn_issn = { ISSN 0168-0072},
year = {2017},
month = {October},
refereed = {yes},
length = {66},
url = {http://www.sciencedirect.com/science/article/pii/S0168007217300490}
}

An overview of PρLog

Besik Dundua, Temur Kutsia, Klaus Reisenberger-Hagmayr

In: Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017, Y. Lierler and W. Taha (ed.), Lecture Notes in Computer Science 10137, pp. 34-49. 2017. Springer, ISBN 978-3-319-51675-2. [pdf]
[bib]
@inproceedings{RISC5416,
author = {Besik Dundua and Temur Kutsia and Klaus Reisenberger-Hagmayr},
title = {{An overview of PρLog}},
booktitle = {{ Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {10137},
pages = {34--49},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-51675-2},
year = {2017},
editor = {Y. Lierler and W. Taha},
refereed = {yes},
length = {16}
}

Nominal Unification of Higher Order Expressions with Recursive Let

Manfred Schmidt-Schauss, Temur Kutsia, Jordy Levy, Mateu Villaret

In: Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016, M. Hermenegildo and P. Lopez-Garcia (ed.), LNCS 10184, pp. 328-344. 2017. Springer, ISBN 978-3-319-63138-7. [pdf]
[bib]
@inproceedings{RISC5438,
author = {Manfred Schmidt-Schauss and Temur Kutsia and Jordy Levy and Mateu Villaret},
title = {{Nominal Unification of Higher Order Expressions with Recursive Let}},
booktitle = {{ Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016}},
language = {english},
series = {LNCS},
volume = {10184},
pages = {328--344},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-63138-7},
year = {2017},
editor = {M. Hermenegildo and P. Lopez-Garcia},
refereed = {yes},
length = {17}
}

Mathematical Aspects of Computer and Information Sciences

Johannes Blömer, Ilias Kotsireas, Temur Kutsia, Dimitris E. Simos, editors

Lecture Notes in Computer Science 10693, 2017. Springer, ISBN 978-3-319-72452-2. [url]
[bib]
@booklet{RISC5518,
author = {Johannes Blömer and Ilias Kotsireas and Temur Kutsia and Dimitris E. Simos and editors},
title = {{Mathematical Aspects of Computer and Information Sciences}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {10693},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-72452-2},
year = {2017},
edition = { },
translation = {0},
length = {462},
url = {https://doi.org/10.1007/978-3-319-72453-9}
}

The RISC Algorithm Language - Tutorial and Reference Manual

Wolfgang Schreiner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, January 2017. [pdf]
[bib]
@techreport{RISC5421,
author = {Wolfgang Schreiner},
title = {{The RISC Algorithm Language - Tutorial and Reference Manual}},
language = {english},
abstract = {This report documents the RISC Algorithm Language (RISCAL). RISCAL is a languageand associated software system for describing (potentially nondeterministic) mathematicalalgorithms over discrete structures, formally specifying their behavior by logical formulas(program annotations in the form of preconditions, postconditions, and loop invariants),and formulating the mathematical theories (by defining functions and predicates and statingtheorems) on which these specifications depend. The language is based on a type systemthat ensures that all variable domains are finite; nevertheless the domain sizes may dependon unspecified numerical constants. By instantiating these constants with values, all algo-rithms, functions, and predicates become executable, and all formulas become decidable.Indeed the RISCAL software implements a (parallel) model checker that allows to verifythe correctness of algorithms and the associated theories with respect to their specificationsfor all possible input values of the parameter domains.},
year = {2017},
month = {January},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
length = {70}
}

MK-fuzzy Automata and MSO Logics

Manfred Droste, Temur Kutsia, George Rahonis, Wolfgang Schreiner

In: 8th Symposium on Games, Automata, Logics and Formal Verification (GandALF’17), P. Bouyer, A. Orlandini, P. San Pietro (ed.), Electronic Proceedings in Theoretical Computer Science (EPTCS) 256, pp. 106-120. September 2017. Rome, Italy, September 22-27, ISSN 2075-2180. [pdf]
[bib]
@inproceedings{RISC5470,
author = {Manfred Droste and Temur Kutsia and George Rahonis and Wolfgang Schreiner},
title = {{MK-fuzzy Automata and MSO Logics}},
booktitle = {{8th Symposium on Games, Automata, Logics and Formal Verification (GandALF’17)}},
language = {english},
abstract = {We introduce MK-fuzzy automata over a bimonoid K which is related to the fuzzification of theMcCarthy-Kleene logic. Our automata are inspired by, and intend to contribute to, practical applicationsbeing in development in a project on runtime network monitoring based on predicate logic. We investigate closure propertiesof the class of recognizable MK-fuzzy languages accepted by MK-fuzzy automata as well asof deterministically recognizable MK-fuzzy languages accepted by their deterministic counterparts.Moreover, we establish a Nivat-like result for recognizable MK-fuzzy languages. We introduce anMK-fuzzy MSO logic and show the expressive equivalence of a fragment of this logic with MK-fuzzyautomata, i.e., a B¨uchi type theorem},
series = { Electronic Proceedings in Theoretical Computer Science (EPTCS)},
volume = {256},
pages = {106--120},
address = {Rome, Italy, September 22-27},
isbn_issn = {ISSN 2075-2180},
year = {2017},
month = {September},
editor = {P. Bouyer and A. Orlandini and P. San Pietro},
refereed = {yes},
keywords = {Many-valued logic, fuzzy logic, MSO logic, runtime monitoring.},
sponsor = {The project “LogicGuard II: The Optimized Checking of Time-Quantified Logic Formulas with Applications in Computer Security” is sponsored by the FFG BRIDGE program, project No. 846003.},
length = {15}
}

Modeling RF-Based Sensor Networks by Using Dual-Source Retrial Queueing Systems

Ovidiu Constantin Novac, Tamás Bérczes, Attila Kuki, Ádám Tóth, Wolfgang Schreiner

In: ICEMES 2017, 14th International Conference on Engineering of Modern Electric Systems, Oradea, Romania, June 1–2, 2017, Mircea Gordan, Teodor Leuca, Florin Constantinescu (ed.), pp. 149-153. 2017. IEEE Xplore, ISBN 978-1-5090-6073-3. [url]
[bib]
@inproceedings{RISC5480,
author = {Ovidiu Constantin Novac and Tamás Bérczes and Attila Kuki and Ádám Tóth and Wolfgang Schreiner},
title = {{Modeling RF-Based Sensor Networks by Using Dual-Source Retrial Queueing Systems}},
booktitle = {{ICEMES 2017, 14th International Conference on Engineering of Modern Electric Systems, Oradea, Romania, June 1–2, 2017}},
language = {english},
abstract = {Here, we would like to study the efficiency and utilization of radio frequency (RF) transmission in wireless sensor networks. A new dual source queueing model (with finite and infinite numbers of sensors) is introduced in order to obtain the most frequently studied system performance characteristics (e.g. mean response time, average number of jobs waiting for transmission, and the utilization of the RF unit). The different types of sensors form the “sources” and the RF unit forms the “central servicing node” of this model. The elements of the sensor fields are classified according to their working purposes: The first class is the “Emergency” or “Special” class which is responsible to notify special rare events (e.g. fire alarms). The other class is the “Standard” class where sensors measure data from standard conventional events or occurrences (eg. motion detection, wind speed, level of darkness etc). For energy efficiency reasons the Central Unit (or Radio Frequency Unit - RFU) might switch into a reduced functioning mode. This reduced communication mode is for saving energy. The transmissions are closed in this mode. Returning from the reduced mode two cases are considered and two models are created to compare their steady-state system performance characteristics: In the first model, the RF transmission is available randomly to the sensor nodes (“Non-Controlled” case). In the other case, the Central Unit jobs which come from the Special class, can use the wireless service immediately (“Controlled” case).},
pages = {149--153},
publisher = {IEEE Xplore},
isbn_issn = {ISBN 978-1-5090-6073-3},
year = {2017},
editor = {Mircea Gordan and Teodor Leuca and Florin Constantinescu},
refereed = {yes},
keywords = {wireless sensors, performance evaluation, retrial queueing, stochastic simulation },
length = {5},
url = {https://doi.org/10.1109/EMES.2017.7980402}
}

Validating the Formalization of Theories and Algorithms of Discrete Mathematics by the Computer-Supported Checking of Finite Models

Alexander Brunhuemer

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, September 2017. Bachelor Thesis. [pdf]
[bib]
@techreport{RISC5485,
author = {Alexander Brunhuemer},
title = {{Validating the Formalization of Theories and Algorithms of Discrete Mathematics by the Computer-Supported Checking of Finite Models}},
language = {english},
abstract = {The goal of this Bachelor’s thesis is the formal specification and implementation of centraltheories and algorithms in the field of discrete mathematics by using the RISC AlgorithmLanguage (RISCAL), developed at the Research Institute for Symbolic Computation (RISC).This specification language and associated software system allow the verification of specifications,by using the concept of finite model checking. Validation on finite models is intendedto serve as a foundation layer for further research on the corresponding generalized theorieson infinite models.This thesis results in a collection of specifications of exemplarily chosen formalized algorithmsof set theory, relation and function theory and graph theory. The algorithms arespecified in different ways (implicit, recursive and procedural), to emphasize the correspondingconnections between them.The evaluation and validation of implemented theories is demonstrated on Dijkstra’s algorithmfor finding a shortest path between vertices in a graph.},
year = {2017},
month = {September},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
length = {88},
type = {Bachelor Thesis}
}

2016

Practical Event Monitoring in the LogicGuard Framework

Wolfgang Schreiner, David Cerna, Temur Kutsia, Michael Krieger, Bashar Ahmad, Helmut Otto, Martin Rummerstorfer, Thomas Gössl

In: embedded world Conference 2016, February 23-25 2016, Nürnberg, Germany, Matthias Sturm et al. (ed.), pp. -. February 2016. Design & Elektronik, Haar, Germany, ISBN 978-3-645-50159-0. [pdf]
[bib]
@inproceedings{RISC5261,
author = {Wolfgang Schreiner and David Cerna and Temur Kutsia and Michael Krieger and Bashar Ahmad and Helmut Otto and Martin Rummerstorfer and Thomas Gössl},
title = {{Practical Event Monitoring in the LogicGuard Framework}},
booktitle = {{embedded world Conference 2016, February 23-25 2016, Nürnberg, Germany}},
language = {english},
abstract = {We describe further progress on the previously introduced LogicGuard specification language and execution framework. This framework generates from a high-level logic specification of a desired property of a stream of events an executable program that observes the stream in real time for violations of the property. While previous presentations were based on an early and incomplete prototype, we are now able to report on some practical applications of the operational framework in the context of network security. As a startup example, we present the “Rogue DHCP” scenario where a device illicitly poses as a DHCP server in order to feed newly connected devices with wrong connectivity information; the monitor detects this attack by looking for duplicate offers to the same DHCP client, of which one is from the attacker. Our main scenario is “Dynamic DNS (DDNS) Cache Poisoining” where an attacker poses as a DDNS client and feeds the DDNS server with wrong DNS update information; the monitor detects this attack by learning about the frequency of legitimate DDNS updates and reporting updates that occur significantly earlier than expected.},
pages = {--},
publisher = {Design & Elektronik},
address = {Haar, Germany},
isbn_issn = {ISBN 978-3-645-50159-0},
year = {2016},
month = {February},
editor = {Matthias Sturm et al.},
refereed = {no},
keywords = {formal methods, runtime verification, event processing},
length = {7}
}

Benchmarks and Performance Analysis of the LogicGuard Framework

Bashar Ahmad, Michael Krieger

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, June 2016. [pdf]
[bib]
@techreport{RISC5370,
author = {Bashar Ahmad and Michael Krieger},
title = {{Benchmarks and Performance Analysis of the LogicGuard Framework}},
language = {english},
abstract = {This paper presents benchmarks, performance measurements and analysisfor LogicGuard framework. The specification and data used to performthe benchmarks are all artificial and were designed to show variouscomplexity levels. For this purpose, a set of parameters was defined togenerate specifications and sample data, which include quantifier depth,search direction, windows size and delay. A set of tools was designed andimplemented to perform the benchmarks and the analysis of the results.In addition to the LogicGuard software, a tool to generate specificationsbased the performance parameters, a tool to process the measurementsand lastly a tool to analyse, extrapolate and plot the results were developed.The results presented show the resource cost in terms of processingtime per message, number of instances and memory usage. To be ableto capture the performance of LogicGuard specification as accurately aspossible, the external function used for monitoring was designed to returnas fast as possible such that the time needed for external processing canbe neglected. Further analysis using polynomial extrapolation is appliedto understand the behaviour of the framework.},
year = {2016},
month = {June},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria},
sponsor = {Supported by the FFG BRIDGE program by the project 846003 “LogicGuard II”.},
length = {26}
}

Loading…