Search

Believed to be a practical solution to eliminate the possibilities of any learning gap to befall, the adaption of online learning specifically the implementation of the synchronous mode of teaching and learning has been practiced in various universities in the arena of education amidst the covid-19 outbreak. In light of this, the present study sought to investigate the different perspectives of would-be language teachers towards synchronous learning. Moreover, this investigation aimed to determine the challenges encountered by the students during the course of learning. The participants of the study were seven students in the tertiary level taking a bachelor’s degree either in English or Filipino. Essentially, a descriptive qualitative research design was employed and individual in-depth interviews were conducted. Furthermore, thematic analysis was utilized to analyze the data gathered. With reference to the findings of this study, it has been noted that the respondents perceive synchronous learning differently, which includes both positive and negative remarks. In addition, internet connectivity issues, limited interaction in virtual platforms, technical difficulties, distractions in the environment, and lack of gadgets were the evident challenges experienced by the students during synchronous learning sessions.

The coronavirus pandemic has had a significant impact in almost all areas of human activity around the world with education being unquestionably affected as well. Universities and Vocational Training Institutes have been forced to close their doors in an effort to stop the spread of the COVID-19 virus. To ensure pedagogical continuity, distance learning courses have been recommended as immediate alternatives. The purpose of this contribution is to investigate how students of Vocational Training Institutes perceive distance education and effectiveness of online foreign language teaching. To this end, a quantitative research based on an online survey was conducted, which included 206, students of five (5) public Vocational Training Institutes and different specialties. The questions were intended to examine the participants’ views on the use of platforms and the collaborative tools, the utility of the educational materials and activities proposed, the learning outcomes in the target language, and, the benefits and limitations of distance synchronous language learning.

Esterel is an imperative synchronous language that has found success in many safety-critical applications. Its precise semantics makes it natural for programming and reasoning. Existing techniques tackle either one of its main challenges: correctness checking or temporal verification. To resolve the issues simultaneously, we propose a new solution via a Hoare-style forward verifier and a term rewriting system (TRS) on Synced Effects. The first contribution is, by deploying a novel effects logic, the verifier computes the deterministic program behaviour via construction rules at the source level, defining program evaluation syntactically. As a second contribution, by avoiding the complex translation from LTL formulas to Esterel programs, our purely algebraic TRS efficiently checks temporal properties described by expressive Synced Effects. To demonstrate our method’s feasibility, we prototype this logic; prove its correctness; provide experimental results, and a number of case studies.

The implementation of hard real-time systems involves a lot of steps that are traditionally manual. The growing complexity of such systems and hardware platforms on which they are executed makes increasingly difficult to ensure the correctness of those steps, in particular for the timing properties of the system on multi-core platform. This leads to the need for automation of the whole implementation process. In this thesis, we provide a method for automatic parallel implementation of real-time systems. The method bridge the gap between real-time systems implementation and compilation by integrating parallelization, scheduling, memory allocation, and code generation around a precise timing model and analysis that rely on strong hypothesis on the execution platform and the form of the generated code. The thesis also provides an implementation model for dataflow multithreaded software. Using the same formal ground as the first contribution, the dataflow synchronous formalisms, the model represents multithreaded implementations in a Lustre-like language extended with mapping annotations. This model allows formal reasoning on the correctness of all the mapping decisions used to build the implementation. We propose an approach toward the proof of correctness of the functionality of the implementation with respect to the functional specifications., L'implémentation de systèmes temps-réel implique de nombreuses étapes qui sont jusqu'aujourd'hui faites manuellement. La complexité de tels systèmes et celle des plateformes matérielles sur lesquelles ils s'exécutent rendent de plus en plus difficile d'assurer la correction de ces étapes de conception (en particulier dans de cadre d'exécutions sur plateformes multi-cœurs). Cela rend l'automatisation de tout le processus d'implémentation inévitable. Cette thèse propose une méthode de parallélisation automatique de systèmes temps-réel. La méthode rapproche les domaines du temps-réel et de la compilation en intégrant les étapes de parallélisation, d'ordonnancement, d'allocation mémoire et de génération de code autour d'une analyse et d'un modèle temporel précis qui s'appuient sur des hypothèses fortes sur la plateforme d'exécution et la forme du code généré. Cette thèse propose également un modèle d'implémentation pour du logiciel flot-de-données multithreadé. En utilisant la même base formelle que précédemment (les formalismes flot-de-données synchrones), un modèle représente une implémentation multithreadé dans un langage comme Lustre, étendu avec des annotations de mapping. Cette modélisation permet un raisonnement formel de toutes les décisions d'implémentation et nous proposons une approche vers la preuve de correction de leur fonctionnalité en rapport à leurs spécifications.

Synchronous programming languages emerged in the 1980s as tools for implementing reactive systems, which interact with events from physical environments and often must do so under strict timing constraints. In this report, we encode inside ATS various real-time primitives in an experimental synchronous language called Prelude, where ATS is a statically typed language with an ML-like functional core that supports both dependent types (of DML-style) and linear types. We show that the verification requirements imposed on these primitives can be formally expressed in terms of dependent types in ATS. Moreover, we modify the Prelude compiler to automatically generate ATS code from Prelude source. This modified compiler allows us to solely rely on typechecking in ATS to discharge proof obligations originating from the need to typecheck Prelude code. Whereas ATS is typically used as a general purpose programming language, we hereby demonstrate that it can also be conveniently used to support some forms of advanced static checking in languages equipped with less expressive types., In Proceedings ML/OCaml 2015, arXiv:1702.01872

Owing to the semantic ambiguities, it has hindered the promotion of IEC 61499 in the field of industrial automation. In order to solve the thorny problem, this paper proposes an implementation scheme for performing formal modeling and simulation verification of semantics of functional block networks. Based on the synchrony hypothesis, the formal execution model is defined according to the fixed point semantics assuming that the behavior of a component functional block is monotonic. Subsequently, through specifying the evaluation of function blocks (FBs) as a process of solving the least-fixed point problem and transforming the network topology into a directed graph, a connectivity attenuation-based algorithm is put forward to ascertain the optimal scheduling policy of FBs with the minimum overhead. Finally, by conducting the experiment for an industrial application, the feasibility and validity of the presented implementation scheme is proved.

International audience