CPA: Conference Support Proposal: 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design

为支持学生参加第二届ACM/IEEE协同设计方法和模型国际会议而向NSF CPA集群提出的建议（MEMOCODE.04）随着计算系统变得越来越复杂，集成到日常可用的人工产品中，如手机、汽车、手持设备、医疗假肢和其他广泛的应用中，需要能够保证硬件和软件成功集成的设计方法。功能的正确性和可靠性越来越重要。今天。S计算不再局限于服务器、工作站和桌面计算，而是无处不在，最重要的是在医疗领域，以及安全关键系统，如航空电子控制、汽车控制等。然而，从历史上看，硬件和软件是分开构建的，两者都非常复杂，确保正确构建硬件或软件的方法本身就是研究课题。然而，由于人类社会越来越依赖于无处不在的和普适的计算，我们面临着对形式化和数学技术的需求来建模和分析集成了硬件和软件的系统。2003年，第一届国际ACM/IEEE共同设计的形式化方法和模型（MEMOCODE）会议首次将在软件工程领域应用形式化方法的研究人员，以及那些应用形式化方法来设计和验证硬件系统的研究人员聚集在一起。从小组讨论、主题演讲和非正式讨论中可以感觉到，双方的正式方法实践者在知识、经验和技术方面有很多分享。此外，硬件软件协同设计问题比以往任何时候都需要这种共生关系，这是创建这一系列会议的最初目的。更重要的是，去年（在法国）出席会议的美国科学家认为，与欧洲的倡议和研究活动相比，美国在正式方法的这一重要领域缺乏研究活动。因此，今年的会议将在加利福尼亚州的圣地亚哥举行，以吸引更多的美国参与者，并为美国研究人员创建一个论坛，以交流正式的方法、思想、技术和创造性的举措。本提案寻求NSF的资金支持，以支持首次参加会议的美国研究生或高级本科生，使他们接触到形式化方法的各个方面，并认识到形式化方法在系统设计中的重要性，特别是硬件/软件安全关键系统。美国国家科学基金会的这种支持对智力的影响是，聪明的年轻学生的出勤率将增加，这将推动这个非常重要领域的更多研究工作。欧洲共同体比美国同行取得了更大的进展，因为研究人员对追求正式方法的兴趣程度要小得多。NSF可以为MEMOCODE的教育和研究目标的丰富做出实质性的贡献。除了NSF之外，研讨会还有一些资金用于邀请演讲者和其他费用。NSF资助的更广泛影响是，它将为美国研究人员的学生提供旅行支持，以鼓励研讨会主题的教育和研究。重点将放在资助那些没有其他资金来源的学生参加会议，并将尝试资助代表性不足的群体的成员。

Proposal to NSF CPA Cluster for Supporting Student Travel to the 2nd ACM/IEEE International Conference on Methods & Models for Co-Design (MEMOCODE.04) As computing systems are becoming increasingly complex, integrated to daily usable artifacts such as cell phones, cars, hand-held devices, medical prosthetics and other wide range of applications, the need for design methodologies which can guarantee successful integration of hardware and software, functional correctness and reliability is gaining importance. Today.s computing is no longer limited to servers, work stations and desktop computing, but they are embedded everywhere, most importantly in the medical space, as well as in the safety critical systems such as avionics control, automotive control etc. However, historically hardware and software have been built separately, and both being extremely complex, the methodologies that ensure correct construction of hardware or software are themselves research topics. Yet, we are faced with the need for formal and mathematical techniques to model and analyze systems which integrate both hardware and software, because of the increasing reliance of human society on ubiquitous and pervasive computing. In 2003 the First International ACM/IEEE Formal Methods and Models for Co-Design (MEMOCODE) conference, for the first time, brought together researchers who apply formal methods in software engineering fields, and those who apply formal methods to design and validate hardware systems. It was felt from the panel discussions, key note talks, and informal discussions that formal method practitioners from both sides have a lot of share in terms of knowledge, experience and techniques. Also, the hardware-software co-design problem imposes an ever than before need for this symbiosis, which was the original aims of creating this series of conferences. More importantly, the US researchers present at the conference last year (in France), felt that there is a lack of research activity in this important area of formal methods in the US, compared to the initiatives and research activities in Europe. As a result, this year the conference is being held in San Diego, California, to bring more US participants, and create a forum for US researchers to exchange formal method ideas, techniques and creative initiatives. This proposal seeks financial support from NSF to support US graduate or advanced undergraduate students attending the conference for the first time, so that they get exposure to various aspects of formal methods, and recognize the importance of formal methods in system design, especially hardware/software safety critical systems. The intellectual impact of this support from NSF would be that the increased attendance of bright young students will fuel more research work in this very important area. The European community has made much more progress than their counter parts in the US due to a much less degree of interest by researchers to pursue formal methods. NSF can make substantial contribution to the enrichment of educational and research objectives of MEMOCODE. The workshop has some funding from sources other than NSF for invited speakers and other expenses. Broader Impact of the requested NSF funding is that it will provide travel support for students of US researchers, to encourage education and research in the workshop topic. The emphasis will be on funding students who do not otherwise have funding sources to attend the conference, and an attempt will be made to fund members of underrepresented groups.