Auflistung nach:
Auflistung it - Information Technology 63(5-6) - Oktober 2021 nach Autor:in "Fränzle, Martin"
1 - 4 von 4
Treffer pro Seite
Sortieroptionen
- ZeitschriftenartikelBayesian hybrid automata: Reconciling formal methods with metrology(it - Information Technology: Vol. 63, No. 4, 2021) Kröger, Paul; Fränzle, MartinHybrid system dynamics arises when discrete actions meet continuous behaviour due to physical processes and continuous control. A natural domain of such systems are emerging smart technologies which add elements of intelligence, co-operation, and adaptivity to physical entities. Various flavours of hybrid automata have been suggested as a means to formally analyse dynamics of such systems. In this article, we present our current work on a revised formal model that is able to represent state tracking and estimation in hybrid systems and thereby enhancing precision of verification verdicts.
- ZeitschriftenartikelFunctional verification of cyber-physical systems containing machine-learnt components(it - Information Technology: Vol. 63, No. 4, 2021) Moradkhani, Farzaneh; Fränzle, MartinFunctional architectures of cyber-physical systems increasingly comprise components that are generated by training and machine learning rather than by more traditional engineering approaches, as necessary in safety-critical application domains, poses various unsolved challenges. Commonly used computational structures underlying machine learning, like deep neural networks, still lack scalable automatic verification support. Due to size, non-linearity, and non-convexity, neural network verification is a challenge to state-of-art Mixed Integer linear programming (MILP) solvers and satisfiability modulo theories (SMT) solvers [2], [3]. In this research, we focus on artificial neural network with activation functions beyond the Rectified Linear Unit (ReLU). We are thus leaving the area of piecewise linear function supported by the majority of SMT solvers and specialized solvers for Artificial Neural Networks (ANNs), the successful like Reluplex solver [1]. A major part of this research is using the SMT solver iSAT [4] which aims at solving complex Boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and therefore is suitable to verify the safety properties of a specific kind of neural network known as Multi-Layer Perceptron (MLP) which contain non-linear activation functions.
- ZeitschriftenartikelA sampling-based approach for handling delays in continuous and hybrid systems(it - Information Technology: Vol. 63, No. 4, 2021) Berani Abdelwahab, Erzana; Fränzle, MartinDelays in feedback dynamics of coupled dynamical systems arise regularly, especially in embedded control where the physical plant and the controller continuously interact through digital networks. Systems featuring delays are however notoriously difficult to analyze. Consequently, formal analysis often addresses simplified, delay-free substitute models, risking negligence of the adverse impact of delay on control performance. In this ongoing work, we demonstrate that for continuous systems such as delay differential equations, a major part of the delay-induced complexity can be reduced effectively when adding natural constraints to the model of the delayed feedback channel, namely that it transports a band-limited signal and implements a non-punctual, distributed delay. The reduction is based on a sampling approach which is applicable when the above conditions on the feedback are satisfied. We further discuss the possibilities of lifting this method to mixed discrete-continuous dynamics of delayed hybrid systems and the open issues thereof.
- ZeitschriftenartikelSystem correctness under adverse conditions(it - Information Technology: Vol. 63, No. 4, 2021) Olderog, Ernst-Rüdiger; Fränzle, Martin; Theel, Oliver; Kröger, PaulThis special issue presents seven overview articles on research conducted in the Research Training Group “System Correctness under Adverse Conditions” (SCARE) at the University of Oldenburg.