Politiikan teoria ennen 1900-lukua

Kirjallisuusarvostelu

Liikesodankäynnin teoria suomalaisessa taktiikassa

Tutkimustyön tarkoituksena on selvittää liikesodankäynnin teorian keskeiset periaatteet ja miten ne ilmenevät suomalaisessa pataljoona ja taisteluosasto tason taktiikassa. Tutkimuksen tarkoituksena on saada vastaus pääkysymykseen: miten liikesodankäynnin teoria näkyy suomalaisessa taktiikassa? Tutkimustyö toteutettiin kvalitatiivisena eli laadullisena tutkimuksena. Tutkimusaineisto liikesodankäynnin teorian keskeisistä periaatteista muodostettiin vertailemalla länsimaisten sotateoreetikkojen tulkintoja liikesodankäynnin teoriasta. Niiden ilmentymistä tutkittiin analysoimalla tutkimuksen teko hetkellä voimassa olevia kyseisen tason ohjesääntöjä ja oppaita pataljoona ja taisteluosasto tason ohjeistuksessa. Havainnoinnin kautta kartoitettiin, miten liikesodankäynnin teorian periaatteet ilmenevät sotaharjoituksissa. Harjoitustoiminnassa esiintyviä periaatteita kartoitettiin syvemmin suorittamalla asiantuntijahaastatteluja teemahaastatteluina. Työn merkittävin tutkimusmenetelmä on sisällönanalyysi. Tutkimuksen tuloksina liikesodankäynnin teorian keskeisiksi periaatteiksi muodostuivat neljä teemaa: vaikuttaminen vastustajan heikkouksiin, vastustajan vahvuuksien välttäminen, johtamisen joustavuus ja painopiste. Pataljoona ja taisteluosasto tason oppaissa ja ohjesäännöissä periaatteiden mukaisia toimintatapamalleja löytyy. Ohjesäännöissä ja oppaissa periaatteet näkyvät yksittäisinä toimintoina, mutta eivät muodosta varsinaisesti liikesodankäynnin teorian mukaista kokonaisuutta. Käytännön harjoitustoiminnassa pyritään joukoilla toteuttamaan ohjesääntöjen ja oppaiden mukaisia toimintoja. Pataljoona ja taisteluosasto tason toimintojen harjoittelussa suurimmiksi haasteiksi muodostuvat joukkojen vähäinen määrä harjoituksissa. Liikesodankäynnin teoria näkyy suomalaisessa taktiikassa keskeisesti vastustajan vahvuuksien välttämisessä. Vastustajan vahvuuksien välttäminen ja siihen liittyvät toiminnat nousivat tutkituista teemoista useimmiten esiintyväksi periaatteeksi ohjesäännöissä sekä käytännön harjoitustoiminnassa.

Formal development of resilient distributed systems

Resilience is the property of a system to remain trustworthy despite changes. Changes of a different nature, whether due to failures of system components or varying operational conditions, significantly increase the complexity of system development. Therefore, advanced development technologies are required to build robust and flexible system architectures capable of adapting to such changes. Moreover, powerful quantitative techniques are needed to assess the impact of these changes on various system characteristics. Architectural flexibility is achieved by embedding into the system design the mechanisms for identifying changes and reacting on them. Hence a resilient system should have both advanced monitoring and error detection capabilities to recognise changes as well as sophisticated reconfiguration mechanisms to adapt to them. The aim of such reconfiguration is to ensure that the system stays operational, i.e., remains capable of achieving its goals. Design, verification and assessment of the system reconfiguration mechanisms is a challenging and error prone engineering task. In this thesis, we propose and validate a formal framework for development and assessment of resilient systems. Such a framework provides us with the means to specify and verify complex component interactions, model their cooperative behaviour in achieving system goals, and analyse the chosen reconfiguration strategies. Due to the variety of properties to be analysed, such a framework should have an integrated nature. To ensure the system functional correctness, it should rely on formal modelling and verification, while, to assess the impact of changes on such properties as performance and reliability, it should be combined with quantitative analysis. To ensure scalability of the proposed framework, we choose Event-B as the basis for reasoning about functional correctness. Event-B is a statebased formal approach that promotes the correct-by-construction development paradigm and formal verification by theorem proving. Event-B has a mature industrial-strength tool support { the Rodin platform. Proof-based verification as well as the reliance on abstraction and decomposition adopted in Event-B provides the designers with a powerful support for the development of complex systems. Moreover, the top-down system development by refinement allows the developers to explicitly express and verify critical system-level properties. Besides ensuring functional correctness, to achieve resilience we also need to analyse a number of non-functional characteristics, such as reliability and performance. Therefore, in this thesis we also demonstrate how formal development in Event-B can be combined with quantitative analysis. Namely, we experiment with integration of such techniques as probabilistic model checking in PRISM and discrete-event simulation in SimPy with formal development in Event-B. Such an integration allows us to assess how changes and di erent recon guration strategies a ect the overall system resilience. The approach proposed in this thesis is validated by a number of case studies from such areas as robotics, space, healthcare and cloud domain.

Yhteistoiminnallinen ja yksilömerkityksinen palautevaikutus : substantiivinen teoria palautteesta varusmiesten kouluttajien toimintaympäristössä

Tutkimuksen tavoitteena oli tuottaa substantiivinen teoria palautteesta varusmiesten kouluttajien toimintaympäristössä. Tavoitteena oli kuvata, minkälaisessa palauteympäristössä varusmiesten kouluttaja työskentelee, miten siellä palaute esiintyy ja minkälainen käytännön teoria varusmiesten kouluttajien näkemyksistä voidaan muodostaa palautteesta heidän toimintaympäristössään. Tutkimuksessa haettiin vastausta siihen, mitkä käsitteet kuvaavat varusmiesten kouluttajien perusteella palautetta varusmieskoulutuksen palauteympäristössä, miten käsitteet suhtautuvat toisiinsa nähden ja minkälainen substantiivinen teoria muodostuu palautteesta varusmiesten kouluttajien toimintaympäristössä. Tutkimus on empiiriseen aineistoon perustuva, jossa on induktiivis-deduktiivisesti käytetty grounded theory -menetelmää straussilaisen suuntauksen periaattein. Tutkimuksessa haastateltiin yhteensä 14 eri varusmiesten kouluttajaa teemahaastatteluin. Haastattelut toteutettiin ensin kahdella ryhmähaastattelulla. Saatua aineistoa hyödynnettiin siten, että aineiston analyysin ensimmäisessä vaiheessa avoimella koodauksella saatuja alakategorioita hyödynnettiin yksilöhaastattelurungon laatimisessa. Kaikkien haastattelujen litteroitu aineisto analysoitiin koodaamalla, muodostamalla alakategoriat, kategoriat ja yläkategoriat sekä tunnistamalla niiden väliset suhteet. Substantiivinen teoria kehittyi muodostuneen ydinkategorian ympärille yhdessä edellä mainittujen tekijöiden perusteella. Tutkimuksen tuloksena saatiin yläkategoriat Henkinen voima, Asennekapasiteetti, Palautteen kohtaaminen, Jokapäiväinen vaikuttaminen ja Yhteinen kehittyminen, jotka ovat substantiivi-sen teorian teoreettiset käsitteet. Käsitteiden välisten suhteiden perusteella muodostettiin ydinkategoria Yksilövoimainen ja yksilömerkityksinen palautevaikutus. Tutkimuksen tulokset osoittivat, että palautevaikutus ulottuu laajalle varusmieskoulutuksen toimintaympäristössä ja että monilla tekijöillä on vaikutusta palautevaikutuksen toteutumiseen. Muodostetut teoreettiset käsitteet korostavat yksilöllisellä tasolla asenteen ja palautteen arvostamisen merkitystä palautevaikutuksen toteutumisessa tai toteutumattomuudessa. Yhteistoiminnallisella tasolla korostuu nimensä mukaisesti yhteinen toiminta eli palautevaikutuksen molemminpuolinen työ onnistumisen eteen. Tutkimuksen avulla saatua tietoa voidaan käyttää varusmiesten ja varusmiesten kouluttajien palautetoiminnan ja -osaamisen kehittämiseen sekä vastaamaan varusmiesyksiköiden haasteelliseen koulutustoimintaan ja palautekulttuuriin toimivien käytäntöjen jatkuvassa kehittämisessä.

Formal modelling for digital media distribution

Human beings have always strived to preserve their memories and spread their ideas. In the beginning this was always done through human interpretations, such as telling stories and creating sculptures. Later, technological progress made it possible to create a recording of a phenomenon; first as an analogue recording onto a physical object, and later digitally, as a sequence of bits to be interpreted by a computer. By the end of the 20th century technological advances had made it feasible to distribute media content over a computer network instead of on physical objects, thus enabling the concept of digital media distribution. Many digital media distribution systems already exist, and their continued, and in many cases increasing, usage is an indicator for the high interest in their future enhancements and enriching. By looking at these digital media distribution systems, we have identified three main areas of possible improvement: network structure and coordination, transport of content over the network, and the encoding used for the content. In this thesis, our aim is to show that improvements in performance, efficiency and availability can be done in conjunction with improvements in software quality and reliability through the use of formal methods: mathematical approaches to reasoning about software so that we can prove its correctness, together with the desirable properties. We envision a complete media distribution system based on a distributed architecture, such as peer-to-peer networking, in which different parts of the system have been formally modelled and verified. Starting with the network itself, we show how it can be formally constructed and modularised in the Event-B formalism, such that we can separate the modelling of one node from the modelling of the network itself. We also show how the piece selection algorithm in the BitTorrent peer-to-peer transfer protocol can be adapted for on-demand media streaming, and how this can be modelled in Event-B. Furthermore, we show how modelling one peer in Event-B can give results similar to simulating an entire network of peers. Going further, we introduce a formal specification language for content transfer algorithms, and show that having such a language can make these algorithms easier to understand. We also show how generating Event-B code from this language can result in less complexity compared to creating the models from written specifications. We also consider the decoding part of a media distribution system by showing how video decoding can be done in parallel. This is based on formally defined dependencies between frames and blocks in a video sequence; we have shown that also this step can be performed in a way that is mathematically proven correct. Our modelling and proving in this thesis is, in its majority, tool-based. This provides a demonstration of the advance of formal methods as well as their increased reliability, and thus, advocates for their more wide-spread usage in the future.

Kohtaamisia ajassa. Kulttuurihistoria ja tulkinnan teoria

Kohtaamisia ajassa. Kulttuurihistoria ja tulkinnan teoria -artikkelikokoelma avaa näkökulmia keskusteluun, jossa pohditaan ymmärtämisen ja tulkitsemisen tehtäviä kulttuurihistoriassa. Artikkelikokoelman tavoitteena on hahmottaa kulttuurihistoriallisen tutkimuksen yhteyksiä viime vuosisadan filosofiaan, jossa kulttuuria ja yhteiskuntaa tutkivien erityistieteiden ontologisilla ja epistemologisilla ongelmilla on ollut tärkeä rooli. 1900-luvun fenomenologia ja hermeneutiikka sekä niistä juontuvat ajattelumuodot nousevat tällöin tarkastelun keskiöön. Lisäksi ne tuovat mukanaan aikaisemmat, 1800-luvun historianfilosofiset ajatukset, joita edustavat G. F. W. Hegel ja Friedrich Nietzsche sekä myöhemmät fenomenologiaa ja hermeneutiikkaa kritikoineet suuntaukset. Kokoelma on puheenvuoro kulttuurihistorian metodologiasta käytävässä keskustelussa, jota se yrittää suunnata kohti mahdollisuuksia, joita 1900-luvun filosofia tarjoaa kulttuurihistorialliselle tutkimukselle. Kohtaamisia ajassa on suunnattu niin kulttuurihistorian opiskelijoille ja tutkijoille kuin myös yleisemmin nykyfilosofiasta ja historian teoriasta kiinnostuneille.

Käytännön pilan teoria

Kirjallisuusarvostelu