doc. Dipl.-Ing. Dr. techn. Stefan Ratschan

Pracoviště
ČVUT FIT, Katedra číslicového návrhu
Výzkumná skupina
Digital Design & Dependability Research Group
Osobní stránky
http://www.cs.cas.cz/~ratschan
E-mail
stefan.ratschan@cs.cas.cz

Verifikace složitých systémů

Verification of Complex Systems

Vlak Pendolino z Prahy do Ostravy měl na začátku vážné problémy: občas zastavoval během jízdy kvůli chybě v softwaru. Podobné chyby způsobovaly vážná neštěstí, například havárii raketoplánu Ariane 5 v roku 1996. Náš výzkum je zaměřen na pomoc se v budoucnosti takovým problémům vyhýbat. Nabízíme velké množství témat v této oblasti. Prodrobnosti jsou k nalezení zde: http://www.cs.cas.cz/~ratschan/theses/cz/verification.html

The Pendolino train from Prague to Ostrava had severe problems in its initial phase: from time to time it stopped in the middle of nowhere due to a software bug. Similar bugs have been the cause of more severe incidents, for example the crash of the Ariane 5 rocket in 1996. We are doing research that will help to avoid such problems in the future, and offer a large range of thesis topics in the area. Details can be found here: http://www.cs.cas.cz/~ratschan/theses/en/verification.html

Řešení omezujících podmínek

Constraint Solving

Vyvíjíme software, teorii a algoritmy které umí řešit matematické formule obsahující nelineární rovnice a nerovnice, konjunkce, disjunkce, a logické kvantifikátory. Aplikujeme výslednou technologii v několika oblastech (např. verifikace složitých systémů, výpočet Lyapunových funkcí). Nabízíme velké množství témat v této oblasti. Prodrobnosti jsou k nalezení zde: http://www.cs.cas.cz/~ratschan/theses/cz/constraint_solving.html

We are developing software, theory, and algorithms that can solve mathematical constraints consisting of non-linear equalities and inequalities, conjunctions, disjunctions, and logical quantifiers. We apply the constraint solving technology in several areas (e.g., verification of complex systems, computation of Lyapunov functions), and offer a large range of thesis topics in the area. Details can be found here: http://www.cs.cas.cz/~ratschan/theses/en/constraint_solving.html

Proveditelné specifikace

Executable Specification

Jedna z nedostatků klasických metod pro specifikaci softwarových požadavků je obtížnost ověření konzistence a adekvátnosti specifikací. Softwarové inženýrství reagovalo na tuto skutečnost různými metodami (např. model based software engineering, agile software development, executable algebraic specification), které dovolují vidět praktické chování specifikací co nejdřív ve vývojovém procesu. Tyto metody ale dělají kompromisy ohledně jiných aspektů např. týkající se expresivity anebo preciznosti. V rámci tohoto tématu student navrhne formální jazyk, který splní dva na první pohled protichůdné cíle:

• Jazyk má expresivitu tak vysokou aby mohl sloužit k pohodlnému psaní specifikací

• Specifikace v tomto jazyku se dají provést podobně jako programy v obvyklém programovacím jazyku

Klíč pro současné splnění obou cílí budou anotace, kterými uživatel jazyku poskytuje informaci o exekuci specifikace tak, aby zvýšená snaha o psaní anotací měla za důsledek zvýšenou účinnost exekuce. První krok bude vývoj nástroje pro výuku, který dovoluje studentům, kteří píšou specifikace jako úkol ve cvičeni, jejich řešení hned i spustit i otestovat.

One of the big drawbacks of classical methods for specifying software requirements is that it is difficult to check the consistency and adequacy of a given specification. The software engineering community has come up with many remedies to this situation (e.g., model based software engineering, agile software development, executable algebraic specification) that usually aim at allowing the user to see the actual behavior of a given specification as early as possible in the development process, but that make compromises in terms of modeling power or precision. In the thesis, the student will design an executable formal specification language that fulfills two seemingly contradicting objectives:

• High modeling capabilities

• Efficient execution

The key to achieving both objectives at the same time will be the design of annotations for the specification language that provide information necessary of efficient execution. Increasing user efforts in writing annotations will result in increasing efficiency of execution of the given specification. In a first step, we will develop a tool that will serve for educational purposes, allowing students to execute specifications they write as assignments.



Poslední změna: 26.4.2019, 14:39