Engineering Deeply Embedded Systems

嵌入式计算机系统在与人们日常生活中重要的物理和生物过程紧密结合方面最具影响力。最值得注意的是，配备微型传感器的联网嵌入式设备可以改善健康和健康的生活方式，以应对加拿大影响最大的领域：慢性病(包括糖尿病和睡眠障碍)和人口老龄化。本项目旨在解决上述应用领域在工程上对可靠、安全、经济的嵌入式设备提出的挑战。为了实现这一目标，我们专注于：1)安全、故障、歧义和噪音容限的嵌入；2)实现质量目标，包括严格的认证标准；3)集成多传感器系统的生产性工程；4)利用新出现的机会。所有这些领域都将通过为我们的应用领域设计具体的系统来推进，这些系统将传递给临床研究，并通过对从试验和我们的模型中获得的数据进行分析研究来增强。具体地说，我们首先考虑集成多传感器设备的设计和验证，除了血糖之外，这些设备还可以跟踪个体的活动水平，并融合不同的数据以增强血糖控制。在区域1中，我们将研究容错和自校准血糖传感器配置；在区域2中，我们将开发用于系统(包括软件)验证和认证目标形式化的形式化和基于断言的技术；在区域3中，我们将研究在临床试验之前允许实际设计闭合的建模方法，以及集成多感官系统及其离散和连续时间和空间操作的高级优化和验证的形式化。指定和验证混合离散-连续系统的核心技术将建立在我们在嵌入式属性检查器以及创新的算法验证和优化方面的进步的基础上，这些创新的算法验证和优化将在几个方向上扩展。最后，将建立适当的抽象和建模方法，以便对这种深度嵌入的系统进行有效的工程设计。

Embedded computer systems are most impactful in a tight integration with physical and biological processes of importance in people's daily lives. Most notably, health and healthy lifestyle can be enhanced by networked embedded devices equipped with miniaturized sensors to deal with the areas of greatest impact in Canada: chronic disease (including diabetes and sleep disorder) and the aging population. This project is aimed at resolving the challenges in engineering dependable, safe and economical embedded devices focusing on the above applications. Towards this goal, we concentrate on: 1) safe, fault-, ambiguity- and noise-tolerant embedding, 2) achieving the quality aims, including strict certification standards, 3) productive engineering of integrated multi-sensory systems and 4) capitalizing on emerging opportunities. All the areas will be advanced by designing concrete systems for our application areas, to be passed to clinical studies and augmented by the analytical investigation of the data obtained from trials and from our models. Specifically, we consider first the design and validation of integrated multi-sensory devices that in addition to glucose track the activity levels of individuals and fuse the dissimilar data to enhance the glucose control. Within area 1, we will investigate fault-tolerant and self-recalibrating glucose sensor configurations, for area 2 we will develop formal and assertion-based techniques for system (including software) validation and the formalization of certification goals and in the area 3 we will investigate the modeling approaches that allow the realistic design closure before clinical trials, as well as the formalisms of the high-level optimization and validation of integrated multi-sensory systems and their discrete- and continuous time and space operation. Core techniques of specifying and validating the hybrid discrete-continuous systems will build on our advances in embedded property checkers and the innovative arithmetic verification and optimization that will be extended in several directions. In the end, suitable abstractions and modeling approaches will be built to allow productive engineering of such deeply embedded systems.