Formal development and quantitative verification of dependable systems

-

Todennäköisyyspohjaisen paloanalyysimenetelmän kehittäminen ydinvoimalaitoksella

Diplomityössä on tutustuttu ydinvoimalaitosten paloriskejä käsittelevään todennäköisyyspohjaiseen turvallisuusanalyysiin. Tavoitteena on ollut Olkiluoto 1 ja 2 laitosyksiköiden paloanalyysimenetelmän kehittäminen. Työssä esitetään paloanalyysin pääpiirteet, kaksi erilaista palotaajuuksien estimointimenetelmää sekä palojen leviämisen arviointimenetelmiä. Palotaajuuksien estimointimenetelmistä keskitytään Berryn menetelmän sekä NUREG/CR-6850-palotaajuuslaskentamenetelmän tarkasteluun. Palon leviämisen arvioinnissa on esitetty kolmen erilaisen virtausteknisen laskentatyökalun perusteet sekä palon leviämistodennäköisyyksiä arvioivan Probabilistic Fire Simulator (PFS) -ohjelman käyttöä. Työn aikana on laskettu molemmilla palotaajuuden estimointimenetelmillä palotaajuuksia eri tyyppisille huonetiloille. Berryn menetelmän palotaajuudet olivat pääosin alhaisempia kuin NUREG/CR-6850-menetelmällä lasketut palotaajuudet. Palon leviämistarkastelussa on tutkittu ydinvoimalaitoksen relehuoneen tulipaloa. PFS:n avulla laskettujen leviämistodennäköisyyksien arvoja on vertailtu TVO:n paloanalyysissa käytettyihin kvalitatiivisiin peittokertoimiin. Palon leviämistodennäköisyys eri osajärjestelmien välillä todettiin suuresti riippuvan analyysissaoletetuista vaurioitumislämpötiloista. Tutkittuja menetelmiä hyödyntäen diplomityössä kehitettiin paloanalyysimenetelmäkuvaus. Menetelmäkuvauksessa huonetilojen paloriskit kartoitetaan aluksi Berryn menetelmällä. Näin kaikille laitoksen huonetiloille saadaan arvioitua palotaajuus sekä paloalkutapahtumaluokkien sydänvauriotaajuus. Seuraavaksi suoritetaan valintamenettely, jossa valitut kriteerit täyttäville huonetiloille tehdään tarkentava palotaajuuslaskenta. Tarkentava palotaajuuslaskenta perustuu NUREG/CR-6850-menetelmän mukaisesti huonetilojen realistisiin syttymislähteisiin. Kriittisimpien huonetilojen osalta palon leviämisen arviointiin on tarkoitus hyödyntää numeerista simulointia.

Todennäköisyyspohjaisen kaapelipaloriskianalyysimenetelmän kehittäminen ydinvoimalaitokselle

Ydinenergian tuottamisessa turvallisuus on tärkeää. Todennäköisyyspohjaisella riskianalyysillä voidaan arvioida turvallisuusvaatimusten täyttymistä eri tilanteissa. Tässä diplomityössä tarkastellaan todennäköisyyspohjaisen riskianalyysin käyttöä ydinvoimalaitoksen kaapelipalojen vaikutusten arvioinnissa. Työn tarkoituksena on omalta osaltaan edistää ydinvoimalaitosten kaapelipaloturvallisuuden parantamista. Työssä esitellään todennäköisyyspohjaisen riskianalyysin ja todennäköisyyspohjaisen paloanalyysin periaatteet sekä nykyiset kaapelipaloanalyysimenetelmät. Olemassa olevien menetelmien pohjalta kehitettiin menetelmä Olkiluoto 1 ja 2 laitosyksiköiden kaapelipaloturvallisuuden arviointiin. Työssä tarkastellaan myös maailmalla sattuneita kaapelipaloja sekä ydinvoimalaitosten palosimulointiin kehitettyä ohjelmistoa. Työssä kehitetty kaapelipaloanalyysi jakautuu kahteen päävaiheeseen: virtapiirien vika-analyysiin ja virtapiirivikojen todennäköisyysanalyysiin. Virtapiirien vika-analyysi käsittää kaapeleiden vikamoodien, virtapiirien vikaantumisluokkien sekä vikaantumisten vaikutuksien määrittämisen. Virtapiirivikojen todennäköisyysanalyysissä määritetään puolestaan vikaantumistodennäköisyydet kaapelipalokokeiden tulosten pohjalta. Kehitettyä analyysimenetelmää sovellettiin esimerkinomaisesti Olkiluoto 1 ja 2 laitosyksiköiden kahdelle eri huonetilalle. Tuloksena saatiin turvallisuudelle tärkeiden järjestelmien virtapiirien vikaantumismallit sekä niiden todennäköisyydet. Tulosten perusteella voidaan todeta, että työssä kehitetty kaapelipaloanalyysimenetelmä toimi hyvin. Tulevaisuudessa menetelmää on tarkoitus hyödyntää Olkiluoto 1 ja 2 -laitosyksiköiden kaapelipaloturvallisuuden arvioinnissa.

Probabilistic contact preferences in protein-ligand and protein-protein complexes

Modeller för intermolekulär växelvärkan utnyttjas brett inom biologin. Analys av kontakter mellan proteiner och läkemedelsforskning representerar typiska tillämpningsområden för dylika modeller. En modell som beskriver sådana molekylära växelverkningar kan utformas med hjälp av biofysisk teori, vilket tenderar att resultera i ytterst tung beräkningsbörda även för enkla tillämpningar. Ett alternativt sätt att formulera modeller är att utnyttja stora databaser som innehåller strukturmätningar gjorda med hjälp av till exempel röntgendiffraktion. Då man använder sig av empiriska mätdata direkt, möjliggör en statistisk modell att osäkerheten och inexaktheten i datat tas till hänsyn på ett adekvat sätt, samtidigt som beräkningsbördan håller sig på en rimligare nivå jämfört med kvantmekaniska metoder som i princip borde ge de optimala resultaten. I avhandlingen utvecklades en 3D modell för numerisk undersökning av intermolekulär växelverkan baserad på Bayesiansk statistik. Modellens syfte är att åstadkomma prognoser för det hurdana eller vilka molekylstrukturer prefereras i en given kontext, d.v.s. är mer sannolika inom ramen för interaktion. Modellen testades i essentiella molekyläromgivningar - en liten molekyl vid sin bindningsplats hos ett protein och en gränsyta mellan proteinerna i ett komplex. De erhållna numeriska resultaten motsvarar väl experimentella resultat som tidigare rapporterats i litteraturen, exempelvis kvalitativa bindningsaffiniteter och kemisk kännedom av vissa aminosyrors rumsliga förmågor att utgöra bindningar. I avhandlingen gjordes ytterligare preliminära tester av den statistiska ansatsen för modellering av den centrala molekylära strukturella anpassningsbarheten. I praktiken är den utvecklade modellen ämnad som ett led i en mer omfattande analysmetod, så som en s.k. farmakofor modell. Molekyylivuorovaikutusten mallintamista hyödynnetään laajasti biologisten kysymysten tarkastelussa. Tyypillisiä esimerkkejä sovelluskohteista ovat proteiinien väliset kontaktit ja lääkesuunnittelu. Vuorovaikutuksia kuvaavan mallin lähtökohta voi olla molekyyleihin liittyvä teoria, jolloin soveltamiseen liittyvä laskenta saattaa olla erityisen raskasta, tai suuri havaintojoukko joka on saatu aikaan esimerkiksi mittaamalla rakenteita röntgendiffraktio menetelmällä. Tilastollinen malli mahdollistaa havaintoaineistossa olevan epätarkkuuden ja epävarmuuden huomioimisen, samalla pitäen laskennallisen kuorman pienempänä verrattuna periaatteessa parhaan tuloksen antavaan kvanttimekaaniseen mallinnukseen. Väitöstyössä kehitettiin bayesiläiseen tilastotieteeseen perustuva 3D malli molekyylien välisten vuorovaikutusten laskennalliseen tarkasteluun. Mallin tehtävä on tuottaa ennusteita sen suhteen, minkä tai millaisten molekyylirakenteiden väliset kompleksit ovat etusijalla, toisin sanoen todennäköisempiä, vuorovaikutustilanteessa. Työssä kehitetyn menetelmän toimivuutta testattiin käyttötarkoituksen suhteen olennaisissa molekyyliympäristöissä - pieni molekyyli sitoutumiskohdassaan proteiinissa sekä rajapinta kahden proteiinin välilllä proteiinikompleksissa. Saadut laskennalliset tulokset vastasivat hyvin vertailuun käytettyjä kirjallisuudesta saatuja kokeellisia tuloksia, kuten laadullisia sitoutumisaffiniteetteja, sekä kemiallista tietoa esimerkiksi tiettyjen aminohappojen avaruudellisesta sidoksenmuodostuksesta. Väitöstyössä myös alustavasti testattiin tilastollista lähestymistapaa tärkeän molekyylien rakenteellisen mukautuvuuden mallintamiseen. Käytännössä malli on tarkoitettu osaksi jotakin laajempaa analyysimenetelmää, kuten farmakoforimallia.

Probabilistic position and orientation estimation of rigid objects using an RGB-D sensor

The recent emergence of low-cost RGB-D sensors has brought new opportunities for robotics by providing affordable devices that can provide synchronized images with both color and depth information. In this thesis, recent work on pose estimation utilizing RGBD sensors is reviewed. Also, a pose recognition system for rigid objects using RGB-D data is implemented. The implementation uses half-edge primitives extracted from the RGB-D images for pose estimation. The system is based on the probabilistic object representation framework by Detry et al., which utilizes Nonparametric Belief Propagation for pose inference. Experiments are performed on household objects to evaluate the performance and robustness of the system.

Design and validation of stateful composite RESTful web services

A web service is a software system that provides a machine-processable interface to the other machines over the network using different Internet protocols. They are being increasingly used in the industry in order to automate different tasks and offer services to a wider audience. The REST architectural style aims at producing scalable and extensible web services using technologies that play well with the existing tools and infrastructure of the web. It provides a uniform set of operation that can be used to invoke a CRUD interface (create, retrieve, update and delete) of a web service. The stateless behavior of the service interface requires that every request to a resource is independent of the previous ones facilitating scalability. Automated systems, e.g., hotel reservation systems, provide advanced scenarios for stateful services that require a certain sequence of requests that must be followed in order to fulfill the service goals. Designing and developing such services for advanced scenarios with REST constraints require rigorous approaches that are capable of creating web services that can be trusted for their behavior. Systems that can be trusted for their behavior can be termed as dependable systems. This thesis presents an integrated design, analysis and validation approach that facilitates the service developer to create dependable and stateful REST web services. The main contribution of this thesis is that we provide a novel model-driven methodology to design behavioral REST web service interfaces and their compositions. The behavioral interfaces provide information on what methods can be invoked on a service and the pre- and post-conditions of these methods. The methodology uses Unified Modeling Language (UML), as the modeling language, which has a wide user base and has mature tools that are continuously evolving. We have used UML class diagram and UML state machine diagram with additional design constraints to provide resource and behavioral models, respectively, for designing REST web service interfaces. These service design models serve as a specification document and the information presented in them have manifold applications. The service design models also contain information about the time and domain requirements of the service that can help in requirement traceability which is an important part of our approach. Requirement traceability helps in capturing faults in the design models and other elements of software development environment by tracing back and forth the unfulfilled requirements of the service. The information about service actors is also included in the design models which is required for authenticating the service requests by authorized actors since not all types of users have access to all the resources. In addition, following our design approach, the service developer can ensure that the designed web service interfaces will be REST compliant. The second contribution of this thesis is consistency analysis of the behavioral REST interfaces. To overcome the inconsistency problem and design errors in our service models, we have used semantic technologies. The REST interfaces are represented in web ontology language, OWL2, that can be part of the semantic web. These interfaces are used with OWL 2 reasoners to check unsatisfiable concepts which result in implementations that fail. This work is fully automated thanks to the implemented translation tool and the existing OWL 2 reasoners. The third contribution of this thesis is the verification and validation of REST web services. We have used model checking techniques with UPPAAL model checker for this purpose. The timed automata of UML based service design models are generated with our transformation tool that are verified for their basic characteristics like deadlock freedom, liveness, reachability and safety. The implementation of a web service is tested using a black-box testing approach. Test cases are generated from the UPPAAL timed automata and using the online testing tool, UPPAAL TRON, the service implementation is validated at runtime against its specifications. Requirement traceability is also addressed in our validation approach with which we can see what service goals are met and trace back the unfulfilled service goals to detect the faults in the design models. A final contribution of the thesis is an implementation of behavioral REST interfaces and service monitors from the service design models. The partial code generation tool creates code skeletons of REST web services with method pre and post-conditions. The preconditions of methods constrain the user to invoke the stateful REST service under the right conditions and the post condition constraint the service developer to implement the right functionality. The details of the methods can be manually inserted by the developer as required. We do not target complete automation because we focus only on the interface aspects of the web service. The applicability of the approach is demonstrated with a pedagogical example of a hotel room booking service and a relatively complex worked example of holiday booking service taken from the industrial context. The former example presents a simple explanation of the approach and the later worked example shows how stateful and timed web services offering complex scenarios and involving other web services can be constructed using our approach.

Business Development Efforts and Performance Improvements in SMEs Case Study of Business Development Projects Implemented in SME

Under the circumstances of the increasing market pressure, enterprises try to improve their competitive position by development efforts, and a business development project is one tool for that. There are not many answers to the question of how the development projects launched to improve the business performance in SMEs have succeeded. Theacademic interest in the business development project success has mainly focused on projects implemented in larger organisations rather than in SMEs. The previous studies on the business success of SMEs have mainly focused on new business ventures rather than on existing SMEs. However, nowadays a large number of business development projects are undertaken in existing SMEs, where they can pose a great challenge. This study focuses on business development success in SMEs thathave already established their business. The objective of the present study is to gain a deep understanding on business development project success in the SME-context and to identify the dimensions and factors affecting the project success. Further, the aim is to clarify how the business development projects implemented in SMEs have affected their performance. The empirical evidence is based on multiple case study. This study builds a framework for a generic theory of business development success in the SME-context, based on literature from the areas ofproject and change management, entrepreneurship and small business management, as well as performance measurement, and on empirical evidence from SMES. The framework consists of five success dimensions: entrepreneurial, project preparation, change management, project management and project success. The framework provides a systematic way for analysing the business development project and its impact on the performance and on the performing company. This case evidence indicates that successful business development projects have a balanced, high performance concerning all the dimensions. Good performance in one dimension is not enoughfor the project success, but it gives a good ground for the other dimensions. The other way round, poor performance in one success dimension affects the others, leading to poor performance of the project. In the SME-context the business development project success seems to be dependent on several interrelated dimensions and factors. Success in one area leads to success in other areas, and so creates an upward success spiral. Failure in one area seems to lead to failure in other areas, creating a downward failure spiral. The study indicates that the internal business development projects have affected the SMEs' performance widely also on areas and functions not initially targeted. The implications cover all thesuccess categories: the project efficiency, the impact on the customer, the business success and the future potentiality. With successful cases, the success tends to spread out to areas and functions not mentioned as the project goals, andwith unsuccessful cases the failure seems to spread out widely to the SMEs' other functions. This study also indicates that the most important key factors for successful business development project implementation are the strength of intention, business ability, knowledge, motivation and participation of the employees, as well as adequate and well-timed training provided to the employees.

Mobile robot localization using sonar ranging and wlan intensity maps

 Main goal of this thesis was to implement a localization system which uses sonars and WLAN intensity maps to localize an indoor mobile robot. A probabilistic localization method, Monte Carlo Localization is used in localization. Also the theory behind probabilistic localization is explained. Two main problems in mobile robotics, path tracking and global localization, are solved in this thesis. Implemented system can achieve acceptable performance in path tracking. Global localization using WLAN received signal strength information is shown to provide good results, which can be used to localize the robot accurately, but also some bad results, which are no use when trying to localize the robot to the correct place. Main goal of solving ambiguity in office like environment is achieved in many test cases.

Conservation Laws in Cellular Automata

Conservation laws in physics are numerical invariants of the dynamics of a system. In cellular automata (CA), a similar concept has already been defined and studied. To each local pattern of cell states a real value is associated, interpreted as the “energy” (or “mass”, or . . . ) of that pattern.The overall “energy” of a configuration is simply the sum of the energy of the local patterns appearing on different positions in the configuration. We have a conservation law for that energy, if the total energy of each configuration remains constant during the evolution of the CA. For a given conservation law, it is desirable to find microscopic explanations for the dynamics of the conserved energy in terms of flows of energy from one region toward another. Often, it happens that the energy values are from non-negative integers, and are interpreted as the number of “particles” distributed on a configuration. In such cases, it is conjectured that one can always provide a microscopic explanation for the conservation laws by prescribing rules for the local movement of the particles. The onedimensional case has already been solved by Fuk´s and Pivato. We extend this to two-dimensional cellular automata with radius-0,5 neighborhood on the square lattice. We then consider conservation laws in which the energy values are chosen from a commutative group or semigroup. In this case, the class of all conservation laws for a CA form a partially ordered hierarchy. We study the structure of this hierarchy and prove some basic facts about it. Although the local properties of this hierarchy (at least in the group-valued case) are tractable, its global properties turn out to be algorithmically inaccessible. In particular, we prove that it is undecidable whether this hierarchy is trivial (i.e., if the CA has any non-trivial conservation law at all) or unbounded. We point out some interconnections between the structure of this hierarchy and the dynamical properties of the CA. We show that positively expansive CA do not have non-trivial conservation laws. We also investigate a curious relationship between conservation laws and invariant Gibbs measures in reversible and surjective CA. Gibbs measures are known to coincide with the equilibrium states of a lattice system defined in terms of a Hamiltonian. For reversible cellular automata, each conserved quantity may play the role of a Hamiltonian, and provides a Gibbs measure (or a set of Gibbs measures, in case of phase multiplicity) that is invariant. Conversely, every invariant Gibbs measure provides a conservation law for the CA. For surjective CA, the former statement also follows (in a slightly different form) from the variational characterization of the Gibbs measures. For one-dimensional surjective CA, we show that each invariant Gibbs measure provides a conservation law. We also prove that surjective CA almost surely preserve the average information content per cell with respect to any probability measure.

On Undecidable Dynamical Properties of Reversible One-Dimensional Cellular Automata

Cellular automata are models for massively parallel computation. A cellular automaton consists of cells which are arranged in some kind of regular lattice and a local update rule which updates the state of each cell according to the states of the cell's neighbors on each step of the computation. This work focuses on reversible one-dimensional cellular automata in which the cells are arranged in a two-way in_nite line and the computation is reversible, that is, the previous states of the cells can be derived from the current ones. In this work it is shown that several properties of reversible one-dimensional cellular automata are algorithmically undecidable, that is, there exists no algorithm that would tell whether a given cellular automaton has the property or not. It is shown that the tiling problem of Wang tiles remains undecidable even in some very restricted special cases. It follows that it is undecidable whether some given states will always appear in computations by the given cellular automaton. It also follows that a weaker form of expansivity, which is a concept of dynamical systems, is an undecidable property for reversible one-dimensional cellular automata. It is shown that several properties of dynamical systems are undecidable for reversible one-dimensional cellular automata. It shown that sensitivity to initial conditions and topological mixing are undecidable properties. Furthermore, non-sensitive and mixing cellular automata are recursively inseparable. It follows that also chaotic behavior is an undecidable property for reversible one-dimensional cellular automata.

Communicative and Anticipatory Decision-Making Supported by Bayesian Networks

The purpose of this research is to draw up a clear construction of an anticipatory communicative decision-making process and a successful implementation of a Bayesian application that can be used as an anticipatory communicative decision-making support system. This study is a decision-oriented and constructive research project, and it includes examples of simulated situations. As a basis for further methodological discussion about different approaches to management research, in this research, a decision-oriented approach is used, which is based on mathematics and logic, and it is intended to develop problem solving methods. The approach is theoretical and characteristic of normative management science research. Also, the approach of this study is constructive. An essential part of the constructive approach is to tie the problem to its solution with theoretical knowledge. Firstly, the basic definitions and behaviours of an anticipatory management and managerial communication are provided. These descriptions include discussions of the research environment and formed management processes. These issues define and explain the background to further research. Secondly, it is processed to managerial communication and anticipatory decision-making based on preparation, problem solution, and solution search, which are also related to risk management analysis. After that, a solution to the decision-making support application is formed, using four different Bayesian methods, as follows: the Bayesian network, the influence diagram, the qualitative probabilistic network, and the time critical dynamic network. The purpose of the discussion is not to discuss different theories but to explain the theories which are being implemented. Finally, an application of Bayesian networks to the research problem is presented. The usefulness of the prepared model in examining a problem and the represented results of research is shown. The theoretical contribution includes definitions and a model of anticipatory decision-making. The main theoretical contribution of this study has been to develop a process for anticipatory decision-making that includes management with communication, problem-solving, and the improvement of knowledge. The practical contribution includes a Bayesian Decision Support Model, which is based on Bayesian influenced diagrams. The main contributions of this research are two developed processes, one for anticipatory decision-making, and the other to produce a model of a Bayesian network for anticipatory decision-making. In summary, this research contributes to decision-making support by being one of the few publicly available academic descriptions of the anticipatory decision support system, by representing a Bayesian model that is grounded on firm theoretical discussion, by publishing algorithms suitable for decision-making support, and by defining the idea of anticipatory decision-making for a parallel version. Finally, according to the results of research, an analysis of anticipatory management for planned decision-making is presented, which is based on observation of environment, analysis of weak signals, and alternatives to creative problem solving and communication.

The probabilistic risk analysis of external hazards of an interim storage for spent nuclear fuel

Tässä diplomityössä tehtiin Olkiluodon ydinvoimalaitoksella sijaitsevan käytetyn ydinpolttoaineen allasvarastointiin perustuvan välivaraston todennäköisyysperustainen ulkoisten uhkien riskianalyysi. Todennäköisyysperustainen riskianalyysi (PRA) on yleisesti käytetty riskien tunnistus- ja lähestymistapa ydinvoimalaitoksella. Työn tarkoituksena oli laatia täysin uusi ulkoisten uhkien PRA-analyysi, koska Suomessa ei ole aiemmin tehty vastaavanlaisia tämän tutkimusalueen riskitarkasteluja. Riskitarkastelun motiivina ovat myös maailmalla tapahtuneiden luonnonkatastrofien vuoksi korostunut ulkoisten uhkien rooli käytetyn ydinpolttoaineen välivarastoinnin turvallisuudessa. PRA analyysin rakenne pohjautui tutkimuksen alussa luotuun metodologiaan. Analyysi perustuu mahdollisten ulkoisten uhkien tunnistamiseen pois lukien ihmisen aikaansaamat tahalliset vahingot. Tunnistettujen ulkoisten uhkien esiintymistaajuuksien ja vahingoittamispotentiaalin perusteella ulkoiset uhat joko karsittiin pois tutkimuksessa määriteltyjen karsintakriteerien avulla tai analysoitiin tarkemmin. Tutkimustulosten perusteella voitiin todeta, että tiedot hyvin harvoin tapahtuvista ulkoisista uhista ovat epätäydellisiä. Suurinta osaa näistä hyvin harvoin tapahtuvista ulkoisista uhista ei ole koskaan esiintynyt eikä todennäköisesti koskaan tule esiintymään Olkiluodon vaikutusalueella tai edes Suomessa. Esimerkiksi salaman iskujen ja öljyaltistuksen roolit ja vaikutukset erilaisten komponenttien käytettävyyteen ovat epävarmasti tunnettuja. Tutkimuksen tuloksia voidaan pitää kokonaisuudessaan merkittävinä, koska niiden perusteella voidaan osoittaa ne ulkoiset uhat, joiden vaikutuksia olisi syytä tutkia tarkemmin. Yksityiskohtaisempi tietoisuus hyvin harvoin esiintyvistä ulkoisista uhista tarkentaisi alkutapahtumataajuuksien estimaatteja.

Excessive functions, Appell polynomials and optimal stopping

The main topic of the thesis is optimal stopping. This is treated in two research articles. In the first article we introduce a new approach to optimal stopping of general strong Markov processes. The approach is based on the representation of excessive functions as expected suprema. We present a variety of examples, in particular, the Novikov-Shiryaev problem for Lévy processes. In the second article on optimal stopping we focus on differentiability of excessive functions of diffusions and apply these results to study the validity of the principle of smooth fit. As an example we discuss optimal stopping of sticky Brownian motion. The third research article offers a survey like discussion on Appell polynomials. The crucial role of Appell polynomials in optimal stopping of Lévy processes was noticed by Novikov and Shiryaev. They described the optimal rule in a large class of problems via these polynomials. We exploit the probabilistic approach to Appell polynomials and show that many classical results are obtained with ease in this framework. In the fourth article we derive a new relationship between the generalized Bernoulli polynomials and the generalized Euler polynomials.

Subshifts with Simple Cellular Automata

A subshift is a set of in nite one- or two-way sequences over a xed nite set, de ned by a set of forbidden patterns. In this thesis, we study subshifts in the topological setting, where the natural morphisms between them are ones de ned by a (spatially uniform) local rule. Endomorphisms of subshifts are called cellular automata, and we call the set of cellular automata on a subshift its endomorphism monoid. It is known that the set of all sequences (the full shift) allows cellular automata with complex dynamical and computational properties. We are interested in subshifts that do not support such cellular automata. In particular, we study countable subshifts, minimal subshifts and subshifts with additional universal algebraic structure that cellular automata need to respect, and investigate certain criteria of `simplicity' of the endomorphism monoid, for each of them. In the case of countable subshifts, we concentrate on countable so c shifts, that is, countable subshifts de ned by a nite state automaton. We develop some general tools for studying cellular automata on such subshifts, and show that nilpotency and periodicity of cellular automata are decidable properties, and positive expansivity is impossible. Nevertheless, we also prove various undecidability results, by simulating counter machines with cellular automata. We prove that minimal subshifts generated by primitive Pisot substitutions only support virtually cyclic automorphism groups, and give an example of a Toeplitz subshift whose automorphism group is not nitely generated. In the algebraic setting, we study the centralizers of CA, and group and lattice homomorphic CA. In particular, we obtain results about centralizers of symbol permutations and bipermutive CA, and their connections with group structures.

A case study of the English language teachers’ attitudes toward use of information and communication technology (ICT) in Finland

This qualitative study was aimed at investigating foreign language teachers’ attitudes toward use of information and communication technology (ICT) in their instruction. The insight was gained through the reported experience of ICT implementation by teachers, in what way and for which purpose they refer to use of technology, what kind of support and training they are provided with, and what beliefs they express about the influence of ICT implementation. This case study took place in one of the training schools in Finland. Five teachers participated in semi-structured interviews through a face-to-face approach. The findings demonstrated positive attitudes of teachers toward integration of ICT. The teachers shared their opinions about positive influence that ICT implementation has on both teaching and learning processes. However, they also pointed out the negative sides of ICT use: distraction of the students from usage of technology and technical problems causing frustration to the teachers. In addition, the responses revealed that the teachers are provided with adequate training aimed at enhancing their qualification which is provided with well-timed technology support and colleagues’ collaboration facilitating an efficient and smooth pace of the teaching process. According to the teachers’ opinions ICT integration in education appeared to have changed the role of the teacher. Due to different alterations in the field of ICT development teachers are required to upgrade their skills. The paper concludes with the limitations of the study and the recommendations for conducting further research.