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.