natgillin/translations-raw huggingface dataset:
FORMAL METHODS IN SOFTWARE ENGINEERING
FORMAALMEETODID SÜSTEEMIARENDUSES
Supervisor Prof Jaan Penjam Institute of Cybernetics
Juht prof Jaan Penjam TTÜ Küberneetika Instituut
Centre for Dependable Computing (CDC) unites scientists from different institutions sharing common research interests and working on common themes following a jointly agreed research plan.
Töökindlate Arvutisüsteemide Uurimise Keskus on erinevate teadusasutuste uurimisrühmade võrk, mis ühendab sarnaste uurimiseesmärkidega teadlasi.
In fact, the associated research groups have for years constituted an informal research network that, depending on the prevailing political and financial situation, has worked together organising all-Estonian seminars, conducting projects for supporting computer science higher education (TEMPUS projects) or running international winter schools for graduate students.
Keskusesse ühendatud uurimisrühmad kujutavad endast juba aastaid de facto koos töötanud uurijate võrku, mis sõltuvalt finantsoludest ja teadus- poliitilisest taustast on teinud koostööd üleriigiliste seminaride vormis, arvutiteadusliku hariduse arendamise sildi all (TEMPUS-projektid) või rahvusvaheliste talvekoolide korraldamisel.
The Centre involves scientists from seven institutions:
Keskuse koosseisu kuuluvad teadlased järgmistest teadusasutustest:
Institute of Cybernetics at TUT (IoC),
TTÜ Küberneetika Instituut (IoC),
Strategic supervision is in the hands of an international Advisory Board of four renowned European scientists: Prof Reino Kurki-Suonio, Tampere University of Technology, Finland; Prof Kim G. Larsen, Aalborg University, Denmark; Prof Reinhard Wilhelm, University of Saarland, Germany; Prof José Oliveira, Universidade do Minho, Braga, Portugal.
Tegevuse süstemaatiliseks rahvusvaheliseks hindamiseks ning temaatikaalaseks nõustamiseks on keskusel juhtkomitee, mille moodustavad neli tunnustatud Euroopa teadlast: prof Reino Kurki-Suonio, Tampere Tehnoloogiaüli- kool, Soome; prof Kim G. Larsen, Ǻlborgi Ülikool, Taani; prof Reinhard Wilhelm, Saarimaa Ülikool, Saksamaa; prof José Oliveira, Minho Ülikool, Braga, Portugal.
Type-theoretic and category-theoretic studies of (co)inductive types and (co)recur- sion schemes.
(Ko)induktiivsete tüüpide ja (ko)rekur- siooniskeemide uurimine tüübi- ja kate- gooriateoreetiliste vahenditega.
Development of methods for static analysis and abstract testing methods based on abstract interpretation.
Abstraktse interpretatsiooni põhiste staatilise analüüsi ja abstraktse testimise meetodite arendamine.
Development of methods for stack code validation and type checking in stack-based languages.
Meetodite arendamine magasinikoodi valideerimiseks ja tüübikontrolliks maga- sinipõhistes keeltes.
Development of structural program synthesis methods for systems with distributed architecture.
Programmide struktuurse sünteesi meetodi arendamine hajusarhitektuuriga arvutisüsteemidele.
Development of new hierarchical diagnostic models of digital systems and highly efficient algorithms for test generation, fault grading and design error and fault diagnosis.
Digitaalsüsteemide uute hierarhiliste diagnostikamudelite ja testide genereerimise, rikete analüüsi ning disainivigade ja rikete diagnoosi efektiivsemate meetodite ja algoritmide väljatöötamine.
The Centre is also in charge of several series of all-Estonian seminars (computer science theory days, formal methods seminar days etc.) as well as master classes of invited foreign lectures.
Samuti organiseeritakse süstemaatiliselt üleriigilisi seminare (arvutiteaduse teooriapäevad, formaalmee- todite seminarpäevad jms) ning meistriklasse kutsutud välisõppejõududega.
Currently, 24 PhD students are being supervised by members of CDC.
Praegu on keskuse liikmete juhendamisel 24 doktoranti.
MATHEMATICAL FOUNDATIONS AND PROGRAMMING LANGUAGE TECHNOLOGY
ARVUTITEADUSE MATEMAATILISED ALUSED JA PROGRAMMEERIMISKEELTE TEHNIKA
The main research directions of the group are logic and algebra as the foundational disciplines of theoretical computer science, and programming language theory (semantics, design, implementation).
Uurimisgrupi põhilisteks teadussuundadeks on loogika ja algebra kui teoreetilise arvutiteaduse alusdistsipliinid ning programmeerimiskeelte teooria (semantika, disain, realiseerimine).
More specifically, the group is focusing on structural proof theory and type theory, categorical logic, ordinal analysis, algebraic combinatorics, semiring theory and algebraic automata theory, programming language semantics and programming language implementation, program analysis, incl. type-based methods, semantics-based program manipulation, language-based security.
Konkreetsemalt on uurimisvaldkondadeks struktuurne tõestusteooria ja tüü- biteooria, kategoorne loogika, ordinaalana- lüüs, algebraline kombinatoorika, poolringide teooria ja algebraline automaaditeooria, programmikeelte semantika ja realisatsioon, programmianalüüs, sh tüübipõhised analüüsid, programmide semantikapõhine teisendamine, turvalisus programmikeeltes.
MAIN RESULTS
OLULISEMAID TULEMUSI
From the 8th Estonian Winter School in Computer Science (EWSCS'03) at Palmse.
Eesti Arvutiteaduse Talvekoolist (EWSCS'03 Palmses).
Several constructive foundational mathematical theories (constructive set theory, Martin-Löf’s type theory) have been shown to be realizable into Feferman’s explicit mathematics.
On näidatud mitme konstruktiivse matemaatilise alusteooria (konstruktiivse hulgateooria, Martin-Löfi tüübiteooria) realiseeritavus Fe- fermani eksplitsiitsesse matemaatikasse.
A number of results has been obtained on rewriting on semirings and the algebraic theory of automata.
On uuritud termiümberkirjutamist poolringidel ning algebralist automaaditeooriat.
The group initiated the Estonian computer science theory days that have been held twice a year since autumn 2002.
Grupp on alates sügisest 2002 kaks korda aastas toimuvate Eesti arvutiteaduse teoori- päevade mootoriks.
Research team: Tarmo Uustalu, Peeter Laud, Jaanus Pöial, Olga Sokratova, Mati Tombak (prof), Sergei Tupailo, Varmo Vene; Reimo Palm; Härmel Nestra, Ahti Peder, Tiina Zingel (PhD students).
Koosseis: Tarmo Uustalu (vanemteadur,), Peeter Laud (vanemteadur), Jaanus Pöial (dotsent), Olga Sokratova (vanemteadur), Mati Tombak (prof), Sergei Tupailo (vanemteadur), Varmo Vene (vanemteadur); Reimo Palm (teadur); Härmel Nestra, Ahti Peder, Tiina Zingel (doktorandid).
Abel, A., Matthes, R., Uustalu, T. Generalized iteration and coiteration for higher-order nested datatypes.
Abel, A., Matthes, R., Uustalu, T. Generalized iteration and coiteration for higher-order nes- ted datatypes.
Barthe, G., Giménez, E., Frade, M. J., Pinto, L., Uustalu, T. Type-based termination of recursive definitions.
Barthe, G., Giménez, E., Frade, M. J., Pinto, L., Uustalu, T. Type-based termination of recur- sive definitions.
14, 1, 97 141 (2004).
14, 1, 97-141 (2004).
Symp. on Programming, ESOP 2003, Lect.
Symp. on Program- ming, ESOP 2003, Lect.
Sokratova, O. The Mal’cev lemma and rewriting on semirings.
Sokratova, O. The Mal’cev lemma and rewri- ting on semirings.
255, 1- 2, 611-614 (2001).
255, 1-2, 611-614 (2001).
Logic 120, 1-3, 165-196 (2003
Logic 120, 1-3, 165-196 (2003).
To meet the high requirements on the reliability of complex systems and to speed up productivity of software development teams, methods for getting provably correct programs are needed.
Keerukatele süsteemidele esitatavate töö- kindlusenõuete rahuldamiseks ja produktiivsuse saavutamiseks süsteemide realiseerimisel vajatakse nii meetodeid korrektsete programmide saamiseks kui ka efektiivseid tarkvaratehnikaid.
Formal proof theory provides a basis for two different approaches to correct software development: program construction (program is derived from its specification) and program verification (program is proven to meet requirements of the specification).
Formaalne tõestusteooria on aluseks kahele erinevale korrektse tarkvara loomise mudelile: programmide automaatne genereerimine tema spetsifikatsioonist ja verifitseerimine (tõestatakse programmi vastavus spetsifikatsioonile).
In practice, a variety of combinations of these two diametrically opposed approaches is used.
Praktikas kasutatakse nende kahe vastandliku lähenemise mitmesuguseid kombinatsioone.
The main aim of this research is studying logic, algebra and systems theory based methods for proving properties and synthesising programs and systems, and also studying properties of the proof methods themselves.
Töörühma eesmärgiks on uurida loogikal, al- gebral ja süsteemiteoorial põhinevaid programmide omaduste tõestamise ja programmide sünteesi meetodeid, samuti arendada automaattõestuse tehnikaid.
Current research is addressing developing techniques and tools applicable for obtaining both transformati- onal and reactive (embedded) systems.
Aktuaalne on meetodite ja vahendite loomine nii transfor- matsiooniliste kui reaktiivsete (reaalaja-) süsteemide arendamiseks.
Research of this team is also focused on formal description and analysis methods of time-sensitive multi- agent systems, and on methods for assessment of structural and behavioural properties of time- sensitive software.
Töörühm on muuhulgas keskendunud nii interaktiivsete arvutuste mudelitele üldiselt kui ka nn ajatundlike agentsüsteemide formaalsele kirjeldamisele ja analüüsile.
The research team has competence in the areas of proof theory and automated theorem proving, program synthesis, timed and hybrid automata, compositional program verification, correctness by construction techniques, and application domains such as mechanical engineering and control.
Töörühma kompetents langeb valdkondadesse, nagu tõestusteooria ja teoreemide automaatne tõestamine, mudelite teooria ajaga ja hübriid-automaadid, kompositsiooniline programmide verifitseerimine, konstruktsiooniga tagatud korrektsus, tarkvara ajastamisprob- leemide formaalne analüüs ning rakendusvaldkonnad, nagu näiteks masinaehitus ja automaatjuhtimine.
SYNTHESIS OF PROGRAMS
PROGRAMMIDE SÜNTEES
A common formal basis for representing semantics of computations both at the level close to hardware primitives, and at the level of software components is presented.
Esitatud on üldine formaalloogiline meetod arvutuste semantika spetsifitseerimiseks, mis kasutab osistena kas tarkvara või riistvara komponente.
This logic is expressive enough for describing, first, the structure of hierarchical configurations and, second, dataflow both at signal and object level.
Kasutatav loogikaarvutus on küllalt väljendusrikas, et esitada samaaegselt süsteemide hierarhilist struktuuri ja andmevoogu nii signaali kui objekti tasandil.
It is sufficiently efficient for synthesis of large configurations and algorithms from their high-level specifications.
Meetod on küllalt võimas genereerimaks keerukaid konfiguratsioone ja algoritme kõrgtaseme spetsifikatsioonide põhjal.
Automatic knowledge based program construction based on declarative description of ontology of a problem domain has been investigated.
Edasi on arendatud meetodeid programmide automaatseks konstrueerimiseks algoritmide probleemvaldkonna ontoloogia formaalse kirjelduse põhjal.
This is an inductive approach based on the idea to search for the optimal program from among all possible sequences of relations of the computational model using genetic programming techniques.
Lähenemise aluseks on idee valida kõigi arvutusmudelil genereeritavate programmide hulgast opti- maalseim, kasutades diferentsiaalevolutsiooni meetodit (induktiivset programmide sünteesi).
Actually, the same computational models by Tõugu are used for specification of problem ontology that are utilised for knowledge representation in structural program synthesis (deductive approach).
Ontoloogia spetsifitseerimiseks kasutatavad arvutusmudelid on samad, mida kasutatakse ülesannete kirjeldamiseks Enn Tõugu struktuurse programmide sünteesi korral ning see asjaolu loob aluse induktiivse ja deduktiivse meetodi kooskasutamiseks programmide konstrueerimisel.
This research is motivated by utilisation and developing further existing paradigms (program synthesis using intuitionistic propositional calculus, Java language etc.) by increasing their performance via parallel computing.
Töö motivatsiooniks on olemasolevate paradigmade (intuitsionistliku lauseloogika abil programmide genereerimine, Java programmeerimiskeel) edasiarendamine, et kasvatada nende jõudlust paral- leelarvutust kasutades.
Modular structure of the distributed program synthe- sizer.
Hajusprogrammide süntesaatori moodulstruktuur.
Co-operation partners: Royal Institute of Technology in Stockholm, Norwegian University of Science and Technology, Stanford University.
Koostööpartnerid: Rootsi Kuninglik Tehnoloo- giaülikool, Norra Teaduse ja Tehnoloogia- ülikool, Stanfordi Ülikool.
MULTIAGENT SYSTEMS
MULTIAGENTSÜSTEEMID
Towards the fault-tolerant parallel computing models a fault-tolerant communication model for parallel computation package DOUG (Domain Decomposition on Unstructured Grids) has been developed.
Tõrkekindlate paralleelarvutuse mudelite uurimiseks on arendatud edasi paralleelarvu- tuste paketti DOUG (Domain Decomposition on Unstructured Grids).
This prototype implantation has been successfully used in stability assessment of flow simulation with the Navier-Stokes equations.
Paketti on edukalt katsetatud Navier-Stokesi vooluvõrrandite stabiilsusarvutuste realiseerimisel.
Co-operation partners: University of Lübeck, University of Bath, Pennsylvania State University, University of Toulouse.
Koostööpartnerid: Lübecki Ülikool, Bathi Ülikool, Pennsylvania Osariigi Ülikool, Toulouse’i Ülikool.
VERIFICATION OF HYBRID DYNAMIC SYSTEMS
HÜBRIIDSETE DÜNAAMILISTE SÜSTEEMIDE VERIFITSEERIJMINE
New methods have been proposed for construction of finite models for first-order predicate formulas describing real-time systems.
Leiti meetodid lõplike mudelite ehitamiseks reaalaja süsteeme kirjeldatavatele esimest järku predikaatarvutuse valemitele, töötati välja uued mittetõestatavuse näitamise meetodid.
New techniques for proving non-derivability have been found and implemented in the automatic theorem proving system Gandalf.
Loodud meetodid realiseeriti teoreemi- tõestamissüsteemis Gandalf.
The continuously developing module of the abovementioned theorem prover won the yearly international contest of proving systems held as a part of the CADE-19 conference in Miami.
Antud töö käigus valminud ja pidevalt täiustatav moodul nimetatud teoreemitõestamissüsteemis võitis vastava ülesanneteklassi iga-aastasel rahvusvahelisel teoreemitõestajate võistlusel konverentsi CADE-19 raames Miamis USAs.
A representation of taxonomies has been developed that allows using an inference engine for classical logic for systems verification and solving queries in semantic web.
Töötati välja mehhanism taksonoomiate esitamiseks ja kasutamiseks klassikalise teo- reemitõestamise kontekstis, mis on vajalik järeldusmootorite efektiivseks kasutamiseks verifitseerimisülesannete ja semantilise veebi- ga seotud ülesannete lahendamisel.
The first prototype system has been implemented that is able to extract facts and rules from the specifications of correctness of the systems and in several semantic web languages, translating them into first-order logic.
Realiseeriti esimene prototüüpsüsteem, mis suudab mõista fakte ja reegleid süsteemide korrektsust kirjeldavates spetsifikatsioonides ja mitmes erinevas semantilise veebi keeles, teisendades neid esimest järku loogikasse.
Co-operation partners: Chalmers Technical University, Danish Technical University, Ålborg University.
Koostööpartnerid: Chalmersi Tehnikaülikool, Taani Tehnikaülikool, Ålborgi Ülikool.
Graham, I. G., Spence A., Vainikko, E. Parallel iterative methods for Navier-Stokes equations and application to eigenvalue computation.
Graham, I. G., Spence A., Vainikko, E. Paral- lel iterative methods for Navier-Stokes equa- tions and application to eigenvalue compu- tation.
Selic, B., Motus, L. Modeling of real-time software with UML.
Selic, B., Motus, L. Modeling of real-time soft- ware with UML.
INFORMATION SECURITY AND CRYPTOGRAPHY
INFOTURVE JA KRÜPTOGRAAFIA
The main goal of the research is to develop and analyze security solutions for electronic documents and databases, as well as to study theoretical limits of cryptographic security measures.
Uurimistöö põhieesmärk on elektrooniliste dokumentide ja andmebaaside turvalahenduste loomine ja analüüs, samuti teoreetilised piirid turvalisuse saavutamisel krüptograafia meetoditega.
TIME STAMPS
AJATEMPLID
Methods have been studied for producing reliable proofs that an electronic document was created at certain time, without assuming the presence of unconditionally secure third parties.
On uuritud meetodeid, kuidas tagada usaldusväärne tõestus mingi elektroonilise dokumendi loomise aja kohta, eeldamata seejuures tingimusteta turvaliste osapoolte olemasolu.
Interesting theoretical results have been obtained about the limits of mathematically provable security properties of time-stamping schemes.
On saadud ka huvitavaid teoreetilisi tulemusi, mis selgitavad ajatempliskeemide turvalisuse matemaatilise tõestatavuse piire.
It turns out that, without adding additional checking procedures to time-stamping systems, there exists no formal proofs that a time- stamping system is secure, based on collision- resistance of the cryptographic hash function used in the system.
Selgub, et vastupidiselt erinevate teoreetikute seas laialt levinud arvamusele, ei saa ajatemplisüstee- mide turvalisust formaalselt tõestada, lähtudes kasutatava krüptograafilise räsifunktsioo- ni kollisioonivabaduse (collision-resistance) omadusest.
SECURE DATABASES
TURVALISED ANDMEBAASID
It has been studied to what extent and how it is possible to protect data in databases, assumed that the holder of the database is not completely trustworthy.
On uuritud, mil määral ja kuidas on võimalik andmebaasides olevaid andmeid kaitsta, eeldusel, et andmebaasi pidaja ei ole täielikult usaldatav.
The security of databases and registries does not mean just the aspect of confidentiality – data must be readable only for authorized persons – but also the aspect of integrity – a reply of the database to a query must be pro- vably authentic and reflect the actual content of the database at the moment of receiving the query.
Andmebaaside ja registrite turvalisuse all ei mõelda mitte ainult konfidentsiaalsuse aspekti – andmed on kättesaadavad ainult volitatud subjektidele – vaid ka tervikluse aspekti – andmebaasist tehtava päringu vastus peab olema tõestatavalt autentne, st peegeldama andmebaasi tegelikku seisu vastuse moodustamise hetkel.
For example, such a requirement is important, if the replies are used as legal documents.
Viimane on vajalik näiteks siis, kui päringuvastuseid kavatsetakse kasutada juriidiliste dokumentidena.
In addition to external threats (such as hackers) one must account for a possible misbehaviour of the database holder.
Lisaks välistele ohtudele (näiteks häkkerid) tuleb arvestada ka andmebaasi halduri enda väär- käitumist.
Co-operation partners: Helsinki University of Technology.
Koostööpartner Helsingi Tehnikaülikool.
Research team: Ahto Buldas, Peeter Laud Jan Willemson; Sven Laur, Meelis Roos, Jelena Zaitseva (PhD students).
Koosseis: Ahto Buldas (vanemteadur), Peeter Laud (vanemteadur), Jan Willemson (vanemteadur); Sven Laur, Meelis Roos, Jelena Zaitseva (doktorandid).
Ansper, A., Buldas, A., Freudenthal, M., Wil- lemson, J. Scalable and efficient PKI for inter- organizational communication.
Ansper, A., Buldas, A., Freudenthal, M., Willem- son, J. Scalable and efficient PKI for inter- organizational communication.
Ansper, A., Buldas, A., Saarepera, M., Willem- son, J. Improving the availability of time- stamping services.
Ansper, A., Buldas, A., Saarepera, M., Wil- lemson, J. Improving the availability of time- stamping services.
Buldas, A., Laud, P., Lipmaa, H. Eliminating counterevidence with applications to accountable certificate management.
Buldas, A., Laud, P., Lipmaa, H. Eliminating counterevidence with applications to accoun- table certificate management.
Wksh. on Practice and Theory of Public Key Cryptography, PKC 2000, Lect.
Wksh. on Practice and Theory of Public Key Crypto- graphy, PKC 2000, Lect.
DESIGN AND TEST OF DIGITAL SYSTEMS
DIGITAALSÜSTEEMIDE DISAIN JA TESTIMINE
MEDEA (Micro-Electronics Development for European Applications) is a part of the pan-European EUREKA network for cooperative R&D in com- puteraided design (CAD) and design automation.
MEDEA (Micro-Electronics Deve- lopment for European Applications) on osa üleeuroopalisest EUREKA võrgustikust, mis tegeleb digitaalsüsteemide projekteerimise alase teaduskoostööga.
The team is involved in design and test of digital systems, self-testing and fault tolerance.
Grupi uurimissuunda- deks on digitaalsüsteemide projekteerimine ja test, isetestivad arhitektuurid ja tõrkekindlad süsteemid.
The main objective of the research is to develop new efficient methods for modelling, design and test of digital systems to guarantee the efficiency, high quality and fault tolerance of systems in the conditions of ever increasing complexities.
Uurimistöö on suunatud uute efektiivsete meetodite väljatöötamisele digitaalsüsteemide modelleerimiseks, projekteerimiseks ja testiks eesmärgiga tagada pidevalt kasvava keerukusega süsteemide efektiivsus, kvaliteet ja tõrkekindlus.
To achieve this target the team has competence in and is actively working on the following more specific problems: diagnostic models for digital systems, automation of test program generation, fault simulation and fault diagnosis in digital systems, physical defect oriented fault analysis, decompositional design and design error diagnosis in digital systems, analysis and partitioning methods for hardware / software codesign, and development of unified representation of systems for control and memory intensive applications.
DT grupp omab kompetentsust ning tegeleb aktiivselt järgmiste probleemidega: digitaalsüsteemide diagnostilised mudelid, testprog- rammide genereerimise automatiseerimine, rikkesimuleerimine ja diagnostika, füüsikaliste defektide analüüs, dekompositsiooniline projekteerimine, projekteerimisvigade diag-noos, analüüsija tükeldusmeetodid riist-/ tarkvara koosdisainis ning valdavalt mälu- ja juhtosa sisaldavate süsteemide ühtlustatud modelleerimine.
A novel diagnostic model for digital systems based on decision diagrams (DDs) has been introduced into the theory of testing.
On välja töötatud uudne diagnostiline mudel, mis põhineb otsustusdiagrammide (decision diagrams, DD) kasutamisel testiteoorias.
The new model affords generalization of testing problems allowing uniform formal handling of systems on logic, procedural, functional as well as behavioural levels.
Mudel võimaldab üldistada diagnostikaproblee- me, lubades ühtlustatud süsteemikäsitlust loogikatasemel, protseduursel, funktsionaalsel ning käituvuslikul tasemel.
Introduction of the new class of structurally synthesized binary DDs (SSBDDs), as well as discovering several interesting properties of SSBDDs afforded to increase the efficiency of algorithms for test generation, fault simulation, and fault diagnosis.
Pakuti välja uudne mudel – struktuurselt sünteesitud binaarsed otsustusdiagrammid (structurally synthesized binary DD ehk SSBDD) koos omadustega, mis võimaldavad tõsta testigenereerimise, rikkesimuleerimise ja -diagnostika algoritmide jõudlust.
A new hierarchical approach to test generation for digital systems based on using the DD-model was proposed.
On välja pakutud uudne hierarhiline lähenemine digitaalsüsteemide testigenereerimi- sele, mis põhineb DD mudeli rakendamisel.
Combining the high-level efficiency of solving complex deterministic search problems and medium-level accuracy of fault “transportation” analysis with low-level exact fault activation allowed to reach high efficiency and high quality in test generation.
Kombineerides keerukate determineeritud ot- singualgoritmide jõudluse kõrgtasemel, rikke- levitamistäpsusega kesktasemel ning madal- taseme rikete aktiveerimise täpsuse, saavutati kõrge kvaliteet ja efektiivsus testide genereerimisel.
A uniform approach to solving logic tasks of digital test was developed.
On välja töötatud ühtlustatud lähenemine testiprobleemide lahendamiseks loogikata- semel.