National Library of Finland DSpace Services
Not a member yet
86391 research outputs found
Sort by
Teho-lehti 2/2024
No full textTyötehoseura ry:n jäsen- ja sidosryhmälehti, TEHO-lehtiei saavutettavaei täytä kaikkia saavutettavuusominaisuuksi
Väyläverkon digitaalinen malli ja kaksonen : Vastaavatko nykyiset ja tunnistetut tiedontuotantomenetelmät tieverkon digitaalisen mallin ja kaksosen tarpeita?
Get PDFHugging Face Hub
No full textEsitys Tekoälykahvit kulttuuriperintöammattilaisille -webinaarissa 17.1.2024
Contract-Based Design of Dataflow Programs
Get PDFQuality and correctness are becoming increasingly important aspects of software development, as our reliance on software systems in everyday life continues to increase. Highly complex software systems are today found in critical appliances such as medical equipment, cars, and telecommunication infrastructure. Failures in these kinds of systems may have disastrous consequences. At the same time, modern computer platforms are increasingly concurrent, as the computational capacity of modern CPUs is improved mainly by increasing the number of processor cores. Computer platforms are also becoming increasingly parallel, distributed and heterogeneous, often involving special processing units, such as graphics processing units (GPU) or digital signal processors (DSP) for performing specific tasks more efficiently than possible on general-purpose CPUs. These modern platforms allow implementing increasingly complex functionality in software. Cost efficient development of software that efficiently exploits the power of this type of platforms and at the same time ensures correctness is, however, a challenging task.
Dataflow programming has become popular in development of safetycritical software in many domains in the embedded community. For instance, in the automotive domain, the dataflow language Simulink has become widely used in model-based design of control software. However, for more complex functionality, this model of computation may not be expressive enough. In the signal processing domain, more expressive, dynamic models of computation have attracted much attention. These models of computation have, however, not gained as significant uptake in safety-critical domains due to a great extent to that it is challenging to provide guarantees regarding e.g. timing or determinism under these more expressive models of computation.
Contract-based design has become widespread to specify and verify correctness properties of software components. A contract consists of assumptions (preconditions) regarding the input data and guarantees (postconditions) regarding the output data. By verifying a component with respect to its contract, it is ensured that the output fulfils the guarantees, assuming that the input fulfils the assumptions.
While contract-based verification of traditional object-oriented programs has been researched extensively, verification of asynchronous dataflow programs has not been researched to the same extent. In this thesis, a contract-based design framework tailored specifically to dataflow programs is proposed. The proposed framework supports both an extensive subset of the discrete-time Simulink synchronous language, as well as a more general, asynchronous and dynamic, dataflow language.
The proposed contract-based verification techniques are automatic, only guided by user-provided invariants, and based on encoding dataflow programs in existing, mature verification tools for sequential programs, such as the Boogie guarded command language and its associated verifier. It is shown how dataflow programs, with components implemented in an expressive programming language with support for matrix computations, can be efficiently encoded in such a verifier. Furthermore, it is also shown that contract-based design can be used to improve runtime performance of dataflow programs by allowing more scheduling decisions to be made at compile-time. All the proposed techniques have been implemented in prototype tools and evaluated on a large number of different programs. Based on the evaluation, the methods were proven to work in practice and to scale to real-world programs.Kvalitet och korrekthet blir idag allt viktigare aspekter inom mjukvaruutveckling, då vi i allt högre grad förlitar oss på mjukvarusystem i våra vardagliga sysslor. Mycket komplicerade mjukvarusystem finns idag i kritiska tillämpningar så som medicinsk utrustning, bilar och infrastruktur för telekommunikation. Fel som uppstår i de här typerna av system kan ha katastrofala följder. Samtidigt utvecklas kapaciteten hos moderna datorplattformar idag främst genom att öka antalet processorkärnor. Därtill blir datorplattformar allt mer parallella, distribuerade och heterogena, och innefattar ofta specialla processorer så som grafikprocessorer (GPU) eller signalprocessorer (DSP) för att utföra specifika beräkningar snabbare än vad som är möjligt på vanliga processorer. Den här typen av plattformar möjligör implementering av allt mer komplicerade beräkningar i mjukvara. Kostnadseffektiv utveckling av mjukvara som effektivt utnyttjar kapaciteten i den här typen av plattformar och samtidigt säkerställer korrekthet är emellertid en mycket utmanande uppgift.
Dataflödesprogrammering har blivit ett populärt sätt att utveckla mjukvara inom flera områden som innefattar säkerhetskritiska inbyggda datorsystem. Till exempel inom fordonsindustrin har dataflödesspråket Simulink kommit att användas i bred utsträckning för modellbaserad design av kontrollsystem. För mer komplicerad funktionalitet kan dock den här modellen för beräkning vara för begränsad beträffande vad som kan beksrivas. Inom signalbehandling har mera expressiva och dynamiska modeller för beräkning attraherat stort intresse. De här modellerna för beräkning har ändå inte tagits i bruk i samma utsträckning inom säkerhetskritiska tillämpningar. Det här beror till en stor del på att det är betydligt svårare att garantera egenskaper gällande till exempel timing och determinism under sådana här modeller för beräkning.
Kontraktbaserad design har blivit ett vanligt sätt att specifiera och verifiera korrekthetsegenskaper hos mjukvarukomponeneter. Ett kontrakt består av antaganden (förvillkor) gällande indata och garantier (eftervillkor) gällande utdata. Genom att verifiera en komponent gentemot sitt konktrakt kan man bevisa att utdatan uppfyller garantierna, givet att indatan uppfyller antagandena.
Trots att kontraktbaserad verifiering i sig är ett mycket beforskat område, så har inte verifiering av asynkrona dataflödesprogram beforskats i samma utsträckning. I den här avhandlingen presenteras ett ramverk för kontraktbaserad design skräddarsytt för dataflödesprogram. Det föreslagna ramverket stödjer så väl en stor del av det synkrona språket. Simulink med diskret tid som ett mera generellt asynkront och dynamiskt dataflödesspråk.
De föreslagna kontraktbaserade verifieringsteknikerna är automatiska. Utöver kontraktets för- och eftervillkor ger användaren endast de invarianter som krävs för att möjliggöra verifieringen. Verifieringsteknikerna grundar sig på att omkoda dataflödesprogram till input för existerande och beprövade verifieringsverktyg för sekventiella program så som Boogie. Avhandlingen visar hur dataflödesprogram implementerade i ett expressivt programmeringsspråk med inbyggt stöd för matrisoperationer effektivt kan omkodas till input för ett verifieringsverktyg som Boogie. Utöver detta visar avhandlingen också att kontraktbaserad design också kan förbättra prestandan hos dataflödesprogram i körningsskedet genom att möjliggöra flera schemaläggningsbeslut redan i kompileringsskedet. Alla tekniker som presenteras i avhandlingen har implementerats i prototypverktyg och utvärderats på en stor mängd olika program. Utvärderingen bevisar att teknikerna fungerar i praktiken och är tillräckligt skalbara för att också fungera på program av realistisk storlek.ei tietoa saavutettavuudest
Exploring the Potential of Civilian-based Defence in the Context of Switzerland
Get PDFAim: The aim of the study was to investigate the potential of civilian-based defence
in the context of Switzerland.
Method: A mix of quantitative and qualitative data collection methods were used for
the study. An online questionnaire aiming to measure the population’s perception of
non-violence effectiveness in defending a country and its readiness to participate in
non-violent civil resistance was shared. Semi-structured interviews with relevant
actors were conducted.
Results: The quantitative analysis showed that a large part of the population would
be ready to participate in non-violent civil resistance in case of invasion. It also
showed a significant difference in the perception of violence effectiveness as a
strategy. Qualitative interviews highlighted the limits and assumptions of the current
defence system supporting the argument of exploring civilian-based defence in
Switzerland.
Conclusions: While no blueprint exists for the development of civilian-based
defence, Switzerland’s situation offers favourable circumstances to explore the
potential of civilian-based defence as a defence system. Furthermore, the civilian based defence could compensate for the current defence system’s weaknesse
An evaluation of how web frameworks support developers to build secure applications
No full textAn increasing number of applications are being built for the web. For this task, developers typically use a number of different frameworks to ease and speed up the development. Frameworks can make complex problems easy by providing tools, patterns and abstraction layers, but can frameworks help developers in one often forgotten area: the application’s security?
Vulnerabilities in web applications can originate from many different sources. A vulnerability might exist due to improper implementation, but also due to poor design. A feature that has been designed in an insecure manner, cannot necessarily be made secure even with a perfect implementation.
The purpose of this thesis is to evaluate how modern web frameworks can help developers build more secure applications. What aspects of security is something a framework can independently manage, what kind of tools can a framework provide the developer to guide them build secure software and what parts of the security is such that a framework cannot manage and is left solely as the responsibility of the developer.
An example application using Vaadin Flow and Spring Boot frameworks, both modern Java based tools, was written for this thesis. The example application was then security tested for vulnerabilities described in the OWASP Top Ten list. The purpose of the evaluation was to understand, which vulnerabilities were directly mitigated by the frameworks and which aspects of the application security is something the developers must understand and mitigate themselves.
This thesis found that only a few explicit technical vulnerabilities were mitigated by the frameworks, while some of the vulnerabilities were such that frameworks could guide the developers by providing tools, but could not ensure full mitigation of the vulnerabilities. To properly secure an application, collaboration is needed between software, network, system, and security engineers, and good DevSecOps practices need to be implemented
Protection of Right to Education, and Prohibition on Discrimination within ECHR
No full textThis thesis examines the case law of European court of Human Rights (ECtHR) regarding protection of right to education and prohibition on discrimination in getting education within the European Convention on Human Rights (ECHR). As the ECtHR articulated, it considers any applicable international law while interpreting the Convention provisions, and it regularly refers to various regional instruments. To determine the elements of discrimination, this thesis examines the European framework for non-discrimination.
This thesis will focus on Roma children regarding the discrimination in getting education and access to educational institution by analysing related case law. This is the main issue to analyse in the thesis; nevertheless, to build the structure of this thesis coherently, the thesis will define the concept of "right to education" and "discrimination," as well as explain how courts assess cases of educational violations according to various elements that hinder access to education.
Roma has been known as one of the largest vulnerable groups of the Europe who has been facing constant violation of their rights and has been the victim of discrimination in several fields. Among them, exclusion from education is one of those fields. Exclusion from education takes the form such as refusal from enrolment in school, placing Roma in special school or classes where there are only Roma people, anti-Roma sentiment which impact ethnic segregation. Whatever the cause, it is unacceptable from a perspective of human rights for there to be any ethnic segregation. Thus, this thesis aims to analyses what are the grounds of discrimination under ECHR, how those grounds affect the individual rights to education, and how court interprets the ground of discrimination through cases.
Furthermore, in this thesis, the part of parental right will be discussed as it has been stated in a same Article where right to education (Article 2 Protocol 1) has been mentioned. There are several occurrences where parents have filed the case on behalf of their children violation on right to education, as well as regarding violation of their parental rights. Accordingly, the thesis looks at the cases to find out what grounds the court determines that there has been a violation regarding parental rights and how it influences parents' objections to matters pertaining to their child's education.
Finally, the thesis concludes by examining the role of non-state actors in safeguarding the educational rights of Roma children and ensuring they do not face discrimination in their pursuit of an education
Rantaradan ja Karjaa–Hanko radan infraselvitys
No full textRantarata on Helsingin ja Turun yhdistävä rautatie, jonka liikenne koostuu Helsinki–Turku-kaukojunaliikenteestä sekä Helsingin ja Siuntion välisellä alueella HSL:n lähijunaliikenteestä. Tavaraliikennettä on normaalisti ainoastaan Salo–Turku-välillä. Tässä työssä on tutkittu edellytyksiä uudelle lähijunaliikenteelle Rantaradan eri osissa ratainfrastruktuurin näkökulmasta ja tunnistettu tarpeellisia kehittämistoimenpiteitä liikenteen lisäämisen mahdollistamiseksi. Työssä on käsitelty kahta toisistaan erillistä tarkastelualuetta. Tarkastelualue ”Itä” sisältää rataosuudet Helsinki–Karjaa ja Karjaa–Hanko pois lukien Helsinki–Leppävaara-kaupunkirata. Tarkastelualue ”Länsi” sisältää rataosuuden Salo–Turku. Sekä itäiselle, että läntiselle alueelle muodostettiin kaksi skenaariota. Itäisellä alueella skenaariot eroavat toisis-taan siten, että toisessa tarkasteltava lähiliikenne perustuu suoriin ja toisessa vaihdollisiin yhteyksiin. Läntisellä alueella on periaatteessa tarkasteltu yhtä liikennöintimallia, mutta tarkasteltava vuoroväli ja tarvittava kalustomäärä on kahdessa skenaariossa eri. Helsingin ja Turun välinen kaukojunaliikenne on oletettu nykyisen kaltaiseksi.
Kirkkonummi–Karjaa- ja Karjaa–Hanko-rataosuuksilla ei ole tässä työssä tarkastelluilla aikataulurakenteilla välttämätöntä toteuttaa infrastruktuurin kehittämistoi-menpiteitä. Lähijunaliikenteen nopeuttamiseksi ja junaliikenteen häiriösietoisuuden parantamiseksi voidaan kuitenkin harkita kaksoisraideosuuden rakentamista Siuntion liikennepaikan ympäristöön, mikäli uutta lähijunaliikennettä tulee Kirkkonummi–Karjaa-rataosuudelle merkittävissä määrin. Karjaa–Hanko-välillä henkilöjunaliikenteen vuorovälin lyhentäminen on haastavinta iltapäivän tunteina, jolloin radalla on nykytilanteessa myös paljon tavaraliikennettä.
Tunnin vuorovälillä liikennöitävää lähijunaa varten kaksoisraide koko Turku–Salo-rataosuudella on ylimitoitettu ratkaisu. Kohtausraide Hajalaan on vaadittava mini-mitoimenpide. Nopeampaa ja sujuvampaa liikennöintiä palveleva ratkaisu olisi joko Piikkiön rataoikaisu, jota käyttäen kaukojunat voivat ohittaa Piikkiön taajaman ja kohdata lähijunan, tai pidempi kaksoisraideosuus Hajalan alueelle, jolla lähi- ja kaukojunat voivat kohdata toisensa.
30 minuutin vuorovälillä liikennöivän Turku–Salo-lähijunan toteuttaminen laadukkaasti edellyttää merkittävää kaksoisraideosuuksien rakentamista Salon ja Turun välille. Teknisenä vähimmäisvaatimuksena on noin 11 km pituisen kaksoisraiteen rakentaminen Hajalan alueelle Salon ja Paimion välille sekä noin 6 km pituisen kaksoisraideosuuden rakentaminen Littoisten alueelle. Tarvittavien kaksoisraideosuuksien sijainnit riippuvat voimakkaasti valittavasta aikataulurakenteesta. Kaksoisraideosuuksien yhteispituus on minimissään noin 35 % Salo–Kupittaa-yhteysvälin pituudesta. Riittävän häiriösietoinen liikenne vaatii todennäköisesti tätä enemmän kaksoisraiteen rakentamista
Rantaradan hankearviointi Kauklahti–Karjaa-rataosalla
No full textKauklahti–Karjaa rataosuus muodostaa noin kolmanneksen Helsingin ja Turun välillä kulkevasta rantaradasta, jonka kokonaispituus on noin 196 kilometriä. Pasila–Karjaa-rataosa avattiin yleiselle liikenteelle jo vuonna 1903 ja radalla on paljon elinkaarensa päähän tulleita kohtia. Rata on jouduttu rakentamaan monin paikoin pehmeiköille, joka on aiheuttanut radan painumista. Myös monet tunnelit ja niiden suuaukot ovat huonossa kunnossa.
Kauklahti–Karjaa-rataosan liikenne koostuu kaukoliikenteestä sekä Kauklahti–Siuntio välillä lisäksi lähijunaliikenteestä. Kaukoliikenteessä matkusti Helsingin ja Karjaan välillä 1,59 miljoonaa matkustajaa vuonna 2022. Helsinki–Turku-välillä liikennöi arkivuorokautena 14 kaukojunaa suuntansa. Lähijunaliikenteessä välillä Kauklahti–Siuntio tehdään lisäksi arviolta noin 2 miljoonaa matkaa vuosittain. Kauklahti–Kirkkonummi välillä lähijunia liikennöi arkivuorokautena 46 vuoroa suuntaansa ja Siuntioon asti 9 vuoroa. Hankearvioinnissa käytetyt liikenne-ennusteet perustuvat Helsinki–Turku-käytävän matkustajaennusteeseen vuodelta 2019.
Hankearviointi rataosalla Kauklahti–Karjaa perustuu rantaradan ja Hangon radan tarveselvitykseen, joka valmistui lokakuussa 2023.
Työssä laadittiin erilliset hankearvioinnit radan peruskorjaustoimenpiteille ja kehittämistoimenpiteille. Peruskorjauksen hankevaihtoehtoina olivat toimenpiteiden toteuttaminen ESKA:n valmistumisen jälkeen vuonna 2029 (P-Ve1a) sekä peruskorjaustoimenpiteiden toteuttaminen Espoon kaupunkiradan (ESKA) rakentamisesta aiheutuvien liikennöinnin viiden viikon totaalikatkojen aikana (P-Ve1b). Vertailu-vaihtoehtona (P-Ve0-) oli ettei toimenpiteitä tehdä ollenkaan, vaan nykyisenkaltainen tilanne säilyy kyseisellä rataosuudella. Kaikki peruskorjauksen toimenpiteet ovat kiireellisiä toimenpiteitä, joilla parannetaan junaliikenteen häiriönhallintaa, mahdollistetaan pistemäisten nopeusrajoitusten poistaminen ja pidetään rata liikennöitävässä kunnossa.
Peruskorjaushankkeiden hyöty-kustannussuhteeksi saatiin hankevaihtoehdossa P-Ve1a 0,60 ja hankevaihtoehdossa P-Ve1b 0,92, kun laskelmassa ei oteta huomioon toteuttamistavasta johtuvaa eroa rakentamiskustannuksissa. Korkeammat rakennuskustannukset vaihtoehdossa P-Ve1a kasvattavat eroa vaihtoehtojen kannattavuuden välillä edelleen. Hankearvioinnissa esitetään suositus tehdä peruskor-jaustoimenpiteet Espoon kaupunkiradan liikennekatkojen aikana.
Kehittämisen hankevaihtoehtoina tarkasteltiin viiden erilaisen kehittämistoimenpidekokonaisuuden toteuttamista (K-Ve1) ja vaihtoehtoisesti näiden lisäksi Siuntion kaksoisraiteen toteuttamista (K-Ve2). Kehittämistoimenpiteillä pyritään parantamaan matkaketjuja, matkustusmukavuutta ja lähiliikenteen toimintamahdollisuuksia sekä poistetaan pistemäisiä nopeusrajoituksia. Kehittämisvaihtoehtojen vertailu-vaihtoehdossa (K-Ve0) vain peruskorjauksen toimenpiteet ovat toteutuneet. Molemmissa kehittämisen hankevaihtoehdossa peruskorjauksen toimenpiteet oletettiin toteutuneiksi. Kehittämisvaihtoehtojen hyöty-kustannussuhteeksi saatiin vaihtoehdossa K-Ve1 0,31 ja Siuntion kaksoisraiteen sisältävässä vaihtoehdossa K-Ve2 0,30. Kehittämishankkeiden yhteiskuntataloudellinen kannattavuus jää heikoksi.
Lähijunaliikenteen maltillinen lisääminen ei edellytä Siuntion kaksoisraidetta. Kaksoisraiteen tarve ja yhteiskuntataloudellinen kannattavuus tulee arvioida uudestaan, jos rataosuudelle Kirkkonummi-Karjaa tulee lähijunaliikennettä huomattavasti lisää