The CrAVES project seeks to lay down intellectual foundations for credible autocoding of embedded systems, by which graphical control system specifications that satisfy given open-loop and closed-loop properties are automatically transformed into source code guaranteed to satisfy the same properties. The goal is that the correctness of these codes can be easily and independently verified by dedicated proof checking systems. During the autocoding process, the properties of control system specifications are transformed into proven assertions explicitly written in the resulting source code. Thus CrAVES aims at transforming the extensive safety and reliability analyses conducted by control system engineers, such as those based on Lyapunov theory, into rigorous, embedded analyses of the corresponding software implementations. CrAVES comes as a useful complement to current static software analysis methods, which it leverages to develop independent verification systems. Computers and computer programs used to manage documents and spreadsheets. They now also interact with physical artifacts (airplanes, power plants, automobile brakes and robotic surgeons), to create Cyber-Physical Systems. Software means complexity and bugs - bugs which can cause real tragedy, far beyond the frozen screens we associate with system crashes on our current PCs. Software autocoding is becoming the de facto recommended practice for many safety-critical applications. CrAVES aims to evolve this towards higher standards of quality and reduced design times and costs. Rigorous, mathematical arguments supporting safety-critical functionalities are the cornerstone of CrAVES. Collaborative programs involving high-school teachers will encourage the transmission of this message to STEM education in high-schools through university programs designed for that purpose.

The focus of this project is the efficient implementation of multiple control and non-control automotive applications in a distributed embedded system (DES) with a goal of developing safe, dependable, and secure Automotive CPS. DES are highly attractive due to the fact that they radically enhance the capabilities of the underlying system by linking a range of devices and sensors and allowing information to be processed in unprecedented ways. Deploying control and non-control applications on a modern DES, which uses advanced processor and communication technology, introduces a host of challenges in their analysis and synthesis, and leads to a large semantic gap between models and their implementation. This gap will be filled via the development of a novel CPS architecture by stitching together common fundamental principles of multimodality from real-time systems and related notions of switching in control theory and integrating them into a co-design of real-time platforms and adaptive controllers. This architecture will be validated at the Toyota Technical Center in the context of engine control and diagnostics. The results of this project will provide the science and technology for a foundation in any and all infrastructure systems ranging from finance and energy to telecommunication and transportation where distributed embedded systems are present. In addition to training the graduate and undergraduate students, and mentoring a post-doctoral associate who will gain multi-domain expertise in advanced control, real-time computation and communication, and performance analysis, an inter-school graduate and an integrated summer course will be developed on control in embedded systems and combined with on-going outreach programs at MIT and UPenn for minority and women undergraduate students and K-12 students.

The objective of this research is to develop a cyber-physical system composed of accelerometers and novel machine learning algorithms to analyze data in the context of a set of driving health care applications. The approach is to develop novel machine learning algorithms for temporal segmentation, classification, and detection of subtle elements of human motion. These techniques will allow quantification of human motion and improved full-time monitoring and assessment of medical conditions using a lightweight wearable system. The scientific contribution of this research is in advancing machine learning and human sensing in support of improved medical diagnoses and treatment monitoring by (i) modeling human activity and symptoms through sensor data analysis, (ii) integrating and fusing information from several accelerometers to monitor in real-time, (iii) validating the efficacy of the automated detection through assessments applying the state of the art in diagnostic evaluation, (iv) developing novel machine learning methods for temporal segmentation, classification, and discovery of multiple temporal patterns that discriminate between temporal signals, and (v) providing quality measures to characterize subtle human motion. These algorithms will advance machine learning in the area of unsupervised and semisupervised learning. The driving applications for this research are job coaching for people with cognitive disabilities, tele-rehabilitation for knee osteo-arthritis, assessing variability in balance and gait as an indicator of health of older adults, and measures for assessing Parkinson's patients. This research is highly interdisciplinary and will train graduate students for careers in developing technological innovations in health and monitoring systems.