This paper presents a correct-by-construction synthesis method for generating operating system based device drivers from a formally specified device behavior model. Existing driver development is largely manual using ...
详细信息
ISBN:
(纸本)1581137427
This paper presents a correct-by-construction synthesis method for generating operating system based device drivers from a formally specified device behavior model. Existing driver development is largely manual using an ad-hoc design methodology. Consequently, this task is error prone and becomes a bottleneck in embedded system design methodology. Our solution to this problem starts by accurately specifying device access behavior with a formal model, viz. extended event driven finite state machines. We state easy to check soundness conditions on the model that subsequently guarantee properties such as bounded execution time and deadlock-free behavior. We design a deadlock-free resource accessing scheme for our device access model. Finally, we synthesize an operating system (OS) based event processing mechanism, which is the core of the device driver, using a disciplined methodology that assures the correctness of the resulting driver. We validate our synthesis method using two case studies: an infrared port and the USB device controller for an SA I 100 based handheld. Besides assuring a correct-by -construction driver, the size of the specification is 70% smaller than a manually written driver, which is a strong indicator of improved design productivity.
CAD vendors are always faced with the question of what tools to develop and how much can they charge for them. Designers on the other hand have real problems to solve and before investing in tools they have to assess ...
详细信息
ISBN:
(纸本)1581137427
CAD vendors are always faced with the question of what tools to develop and how much can they charge for them. Designers on the other hand have real problems to solve and before investing in tools they have to assess how much a given tool will actually save them. CAD vendors and designers have to estimate the savings in design time and cost that a tool may provide and compare that with the existing way of doing things, to determine if the investment in tool creation is justified. For example, if a misguided architectural decision causes weeks of delay because of missing performance targets, then a tool for early architectural analysis may be very valuable. system-level design poses exactly these types of questions because it involves optimizations and analyses across many domains, from software, to architecture, to cycle-time, and is done very early in the design cycle where it has a profound impact. How much improvement in productivity and overall design quality (e.g., timing, area, and power) can be attained by current and future generations of system-level tools? If designers believe such improvements can be obtained, are they prepared to pay the appropriate price for the tools? Or do system-level CAD vendors still need to make believers out of designers? This panel will bring together industry experts to review the current and future industry needs for system-level design technologies as well as discuss how much saving in design time and cost such tools can hope to achieve and whether the designers believe the price is right for the return they can get.
The design of next-generation systems running streaming applications is becoming extremely challenging as these sys- tems are executing many real-time applications concurrently. To address this design challenge, predi...
详细信息
ISBN:
(纸本)9781450307154
The design of next-generation systems running streaming applications is becoming extremely challenging as these sys- tems are executing many real-time applications concurrently. To address this design challenge, predictable multi-processor systems-on-chip platforms and accompanying model-based design approaches are being developed. This tutorial presents an overview of future platforms and design approaches needed to design next-generation embedded systems for real-time streaming applications. During the hands-on session the participants apply this theory to a practical example. 2011, Taipei, Taiwan. acm 978-1-4503-0715-4/11/10. Copyright 2011 acm.
Formal theories for real-time systems (such as timed process algebra, timed automata and timed petri nets) have gained great success in the modeling of concurrent timing behavior and in the analysis of real-time prope...
详细信息
Formal theories for real-time systems (such as timed process algebra, timed automata and timed petri nets) have gained great success in the modeling of concurrent timing behavior and in the analysis of real-time properties. However, due to the ineliminable timing differences between a model and its realization, synthesizing a software realization from a model in a predictable way is still a challenging research topic. In this article, we tackle this problem by solving a set of sub-problems. The solution is based on the theoretical results for property prediction proposed in Huang et al. (2003, Real-time property preservation in approximations of timed systems. In: Proceedings of 1stacm and ieeeinternationalconference on formal methods and models for codesign. ieee Computer Society, Los Alamitos, pp 163-171) and Huang (2005, Predictability in real-time system design. PhD thesis, Eindhoven University of Technology, The Netherlands), where quantitative property relations are established between two absolute/relative "close" real-time systems. This theory basically implies that if two systems are "close", they enjoy "similar" properties. These results cannot be directly applied in practice though, because a model and its realization typically have infinitely large absolute and relative timing differences. We show that this infinite time gap can be bridged through a sequence of carefully constructed intermediate time domains. Then the property-prediction results can be applied to any pair of adjacent time domains in the sequence. Consequently, real-time properties of the implementation can be predicted from the model. We propose two parameterized hypotheses to characterize the timing differences in the sequence and to guide a correctness-preserving design process. It is shown that these hypotheses can be incorporated in a concrete tool set. We demonstrate the feasibility of the predictable synthesis approach through the design of a railroad crossing system.
暂无评论