With the advent of exascale architectures maximizing performance while maintaining energy consumption within reasonable limits has become one of the most critical design constraints. This constraint is particularly significant in light of the power budget of 20 MWatts set by the U.S. Department of Energy for exascale supercomputing facilities. Therefore, understanding an application's characteristics, execution pattern, energy footprint, and the interactions of such aspects is critical to improving the application's performance as well as its utilization of the underlying resources. With conventional methods of analyzing performance and energy consumption trends scientists are forced to limit themselves to a manageable number of design parameters. While these modeling techniques have catered to the needs of current high-performance computing systems, the complexity and scale of exascale systems demands that large-scale design-space-exploration techniques are developed to enable comprehensive analysis and evaluations. In this dissertation we present research on performance and energy modeling of current high performance computing and future exascale systems. Our thesis is focused on the design space exploration of current and future architectures, in terms of their reconfigurability, application's sensitivity to hardware characteristics (e.g., system clock, memory bandwidth), application's execution patterns, application's communication behavior, and utilization of resources. Our research is aimed at understanding the methods by which we may maximize performance of exascale systems, minimize energy consumption, and understand the trade offs between the two. We use analytical, statistical, and machine-learning approaches to develop accurate, portable and scalable performance and energy models. We develop application and machine abstractions using Aspen (a domain specific language) to implement and evaluate our modeling techniques. As part of our research we develop and evaluate system-level performance and energy-consumption models that form part of an automated modeling framework, which analyzes application signatures to evaluate sensitivity of reconfigurable hardware components for candidate exascale proxy applications. We also develop statistical and machine-learning based models of the application's execution patterns on heterogeneous platforms. We also propose a communication and computation modeling and mapping framework for exascale proxy architectures and evaluate the framework for an exascale proxy application. These models serve as external and internal extensions to Aspen, which enable proxy exascale architecture implementations and thus facilitate design space exploration of exascale systems. / Ph. D.

In this dissertation, the concept of using domain specific language to develop errorree parallel asynchronous load scheduling protocols for distributed systems is studied. The motivation of this study is rooted in addressing the high cost of verifying parallel asynchronous load scheduling protocols. Asynchronous parallel applications are prone to subtle bugs such as deadlocks and race conditions due to the possibility of non-determinism. Due to this non-deterministic behavior, traditional testing methods are less effective at finding software faults. One approach that can eliminate these software bugs is to employ model checking techniques that can verify that non-determinism will not cause software faults in parallel programs. Unfortunately, model checking requires the development of a verification model of a program in a separate verification language which can be an error-prone procedure and may not properly represent the semantics of the original system. The model checking approach can provide true positive result if the semantics of an implementation code and a verification model is represented under a single framework such that the verification model closely represents the implementation and the automation of a verification process is natural. In this dissertation, a domain specific language based verification framework is developed to design parallel load scheduling protocols and automatically verify their behavioral properties through model checking. A specification language, LBDSL, is introduced that facilitates the development of parallel load scheduling protocols. The LBDSL verification framework uses model checking techniques to verify the asynchronous behavior of the protocol. It allows the same protocol specification to be used for verification and the code generation. The support to automatic verification during protocol development reduces the verification cost post development. The applicability of LBDSL verification framework is illustrated by performing case study on three different types of load scheduling protocols. The study shows that the LBDSL based verification approach removes the need of debugging for deadlocks and race bugs which has potential to significantly lower software development costs.

No description available.

No description available.

Dans de multiples domaines, un nombre grandissant d'applications interagissant avec des entités communicantes apparaissent dans l'environnement pour faciliter les activités quotidiennes~(domotique et télémédecine). Leur impact sur la vie de tous les jours des utilisateurs rend ces applications critiques: leur défaillance peut mettre en danger des personnes et leurs biens. Bien que l'impact de ces défaillances puisse être majeur, la sécurité est souvent considérée comme un problème secondaire dans le processus de développement et est traitée par des approches ad hoc.Cette thèse propose d'intégrer des aspects de sécurité dans le cycle de développement des systèmes d'informatique ubiquitaire. La sécurité est spécifiée à la conception grâce à des déclarations dédiées et de haut niveau. Ces déclarations sont utilisées pour générer un support de programmation afin de faciliter l'implémentation des mécanismes de sécurité, tout en séparant ces aspects de sécurité de la logique applicative. Notre approche se concentre sur le contrôle d'accès aux entités et la protection de la vie privée. Notre travail a été implémenté et fait levier sur une suite outillée existante couvrant le cycle de développement logiciel. / A growing number of environments is being populated with a range of networked devices. Applications leverage these devices to support everyday activities in a variety of areas (e.g., home automation and patient monitoring). As these devices and applications get woven into our everyday activities, they become critical: their failure can put people and assets at risk. Failures can be caused by malicious attacks and misbehaving applications. Although the impact of such situations can be major, security concerns are often considered a secondary issue in the development process, and treated with ad hoc approaches. This thesis proposes to address security concerns throughout the development lifecycle of a pervasive computing system. Security is addressed at design time thanks to dedicated, high-level declarations. These declarations are processed to implement security mechanisms, and to generate programming support to ease the development of the security logic, while keeping it separate from the application logic. Our approach is studied in the context of access control and privacy concerns. Our work has been implemented and leverages an existing software-design language and a suite of tools that covers the software development lifecycle.

Lors du développement des applications ubiquitaires, il est essentiel de définir des politiques de sécurité et de développerdes mécanismes de sécurité pour assurer la confidentialité et l’intégrité des applications. De nombreux langages de spécification de politiques se concentrent uniquement sur leur puissance d’expression. Les défis émergents dans les systèmes ubiquitaires ne peuvent pas être résolus par ces approches. Par exemple, la sensibilité au contexte est un élément central des systèmes ubiquitaires. Les approches existantes tiennent rarement compte des informations contextuelles dans leurs langages. Cette thèse propose une approche générative pour spécifier et implanter les politiques de sécurité dans les applications ubiquitaires. Pour définir une politique de sécurité, nous proposons un langage de spécification qui tient compte des informations contextuelles. Il permet aux développeurs de spécifier les règles de la politique et les entités requises (e.g. la description spatiale, les rôles, le contexte). Les politiques sont implémentés par des systèmes de réécriture, ce qui offre une grande puissance de vérification. Pour appliquer une politique, nous proposons une architecture qui intègre les concepts importants des politiques de sécurité (sujet, contexte, objet) dans des applications ubiquitaires. Pour mettre en oeuvre notre approche, nous avons enrichi une approche existante pour le développement des applications ubiquitaires. La spécification de la politique de sécurité et la description de l’application ubiquitaire enrichie sont utilisées pour générer un canevas de programmation qui facilite l’implémentation des mécanismes de sécurité, tout en séparant les aspects sécurités de la logique applicative. / When developing pervasive computing applications, it is critical to specify security policies and develop security mechanisms to ensure the confidentiality and integrity of the applications. Numerous policy specification languages only focus on their expressive power. The emerging challenges in pervasive computing systems can not be fulfilled by these approaches. For instance, context awareness is a central aspect of pervasive computing systems. Existing approaches rarely consider context information in their language.This thesis proposes a generative approach dedicated to specifying and enforcing security policies in pervasive computingapplications. To specify a policy, we propose a context-aware policy specification language which helps developers to specify policy rules and required entities (e.g. spatial description, roles, context information). Policies are implemented by term rewriting systems which offers great verification power. To enforce a policy, we propose an architecture that embeds important concepts of security policies (subject, object, security related context) into pervasive computing applications. To apply our approach, we enriched an existing approach which is dedicated to develop pervasive computing applications. Based on the policy specification and the enriched pervasive computing application descriptions, a dedicated programming framework is generated. This framework guides the implementation and raises the level of abstraction which can reduce the workloads of developers.

The domain-specific language allows for describing problems of a concrete domain, for which the language is created. This fact implies that a number of languages of this kind grows with a number of problem domains. The use of domain-specific languages brings a necessity to pretty-print these languages, where the concept of pretty-printing consists of code formatting and syntax highlighting. One of tools that allow for creating domain-specific languages is the Xtext framework, which offers only a limited range of tools that are able to define a configuration for pretty-printing. Moreover, these tools are hardly understandable because they are confusing and requires knowledge of Xtext's internals. Thus this thesis introduces a new way of pretty-printing domain-specific languages. The way is based on declarative definition of formatting rules. Furthermore, this thesis helps a user to create formatting rules by utilizing nontrivial heuristics.

In the scope of this thesis, we designed a language for programming education. At first, we described eight existing tools for learning programming and identified key features in the learning process. Second, we designed an educational domain-specific language Eddie. Eddie is suitable for teenagers and adults who want to learn programming. It uses a domain based on Karel the Robot language, where users can control a robot character in a two-dimensional grid. We implemented a prototype of Eddie using the MPS Language Workbench and its projectional editor. The Eddie language gradually introduces loops, conditionals, variables, functions, and objects. Eddie programs can be created, executed and visualized in the Eddie Studio IDE. Powered by TCPDF (www.tcpdf.org)

Malgré des progrès récents, développer une application d'informatique ubiquitaire reste un défi à cause d'un manque de canevas conceptuels et d'outils aidant au développement. Ce défi implique de prendre en charge des objets communicants hétérogènes, de surmonter la complexité des technologies de systèmes distribués, de définir l'architecture d'une application, et d'encoder cela dans un programme. De plus, tester des applications d'informatique ubiquitaire est problématique car cela implique d'acquérir, de tester et d'interfacer une variété d'entités logicielles et matérielles. Ce procédé peut rapidement devenir coûteux en argent et en temps lorsque l'environment ciblé implique de nombreuses entités.Cette thèse propose une méthodologie outillée pour développer et tester des applications d'informatique ubiquitaire. Notre méthodologie fournit tout d'abord le langage de conception DiaSpec. Ce langage permet de définir une taxonomie d'entités spécifiques à un domaine applicatif, s'abstrayant ainsi de leur hétérogénéité. Ce langage inclut également une couche permettant de définir l'architecture d'une application. Notre suite outillée fournit un compilateur qui, à partir de descriptions DiaSpec, génère un canevas de programmation guidant les phases d'implémentation et de test. Afin d'aider à la phase de test, nous proposons une approche de simulation et un outil intégré dans notre méthodologie outillée : l'outil DiaSim. Notre approche utilise le support de test généré par DiaSpec pour tester les applications de manière transparente dans un environnement physique simulé. La simulation d'une application est rendue graphiquement dans un outil de visualisation 2D.Nous avons combiné DiaSim avec un langage dédié permettant de décrire les phénomènes physiques en tant qu'équations différentielles. Cette combinaison nous permet une simulation réaliste des applications d'informatique ubiquitaire. DiaSim a été utilisé pour simuler des applications dans des domaines applicatifs variés. Notre approche de simulation a également été appliquée à un système avionique, démontrant la généralité de notre approche de simulation. / Despite much progress, developing a pervasive computing application remains a challenge because of a lack of conceptual frameworks and supporting tools. This challenge involves coping with heterogeneous devices, overcoming the intricacies of distributed systems technologies, working out an architecture for the application, and encoding it into a program. Moreover, testing pervasive computing applications is problematic because it requires acquiring, testing and interfacing a variety of software and hardware entities. This process can rapidly become costly and time-consuming when the target environment involves many entities.This thesis proposes a tool-based methodology for developing and testing pervasive computing applications. Our methodology first provides the DiaSpec design language that allows to define a taxonomy of area-specific building-blocks, abstracting over their heterogeneity. This language also includes a layer to define the architecture of an application. Our tool suite includes a compiler that takes DiaSpec design artifacts as input and generates a programming framework that supports the implementation and testing stages.To address the testing phase, we propose an approach and a tool integrated in our tool-based methodology, namely DiaSim. Our approach uses the testing support generated by DiaSpec to transparently test applications in a simulated physical environment. The simulation of an application is rendered graphically in a 2D visualization tool.We combined DiaSim with a domain-specific language for describing physical environment phenomena as differential equations, allowing a physically-accurate testing. DiaSim has been used to simulate various pervasive computing systems in different application areas. Our simulation approach has also been applied to an avionics system, which demonstrates the generality of our parameterized simulation approach.

With the widely use of software technique in everyday applications, the correctness of software becomes more and more important. Formal verification is an important method to improve the correctness of software. However, it mainly takes formal languages as its modeling languages, which are based on mathematical logic, automata or graph theory, hard for learning and domain description. That hinders the applications of formal verification in industry. This dissertation investigates the design and practice of domain modeling and verification language EDOLA, to possess all the features of the usability for domain description, reusability and automatic verification. It proposes a three-level design method with the domain knowledge level, the common module level and the verification support level. The main contributions are summarized as follows: 1. In the domain knowledge level, the extraction and representation methods of the domain knowledge on both job-shop scheduling and PLC control software are proposed. It defines domain-specific operators of the job-shop scheduling problem, timed Petri net, etc. for the job-shop scheduling description. It also defines the operators of the scan cycle pattern, the complete environment pattern and five kinds of verification requests for the PLC domain description. It presents the formal semantics of the defined domain-specific operators, for the further EDOLA definition and its automatic verification. 2. In the common module level, the method to define common operators is presented with real-time as an example for common knowledge. It proposes two kinds of basic time operators and four advanced ones, which help EDOLA to describe real-time features easily and make the reusability of EDOLA design among time-sensitive domains possible. 3. In the verification support level, it presents a properties-oriented abstraction strategy, which reduces the state space and exploring space during automatic verifi- cation. It then formulates the encoding rules from EDOLA to first-order logic, thus implements the verification of the models with infinite states, with the help of first-order logic automatic theorem provers. 4. A prototype of the PLC domain modeling and verification language: EDOLA-PLC are developed and its tools are implemented. The tools provide an EDOLA-PLC editor and a compiler with the functionalities like syntax checking, semantics checking and translation-based automatic verification. 5. A case study of the EDOLA-PLC language on a dock fire-fighting control system is presented. It indicates that EDOLA-PLC is easy to describe both the PLC domain knowledge and the properties to be verified; is easy to describe the common knowledge: real-time and can be verified automatically. The results show that the abstraction strategy adopted in the verification support level of EDOLA-PLC improves the efficiency of automatic verification.