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.