形式化开发网络中心实时操作系统

需积分: 15 50 浏览量更新于2024-07-17 收藏 2.94MB PDF 举报

"Formal Development of a Network-Centric RTOS" 本书详细介绍了OpenComRTOS，这是一种正式开发的网络中心实时操作系统（RTOS），它在嵌入式软件工程领域中首次展示了形式化方法的应用价值。OpenComRTOS的独特之处在于，它涵盖了从需求、规范到最终执行平台的完整产品开发范围，并且与如IEC61508等安全相关工程标准兼容，从而确保了软件的可靠性和高性能。在实时操作系统（RTOS）的开发中，形式化方法是一种严谨的系统设计和验证技术，它利用数学逻辑来精确地描述软件的行为和性质。通过这种方法，开发者能够确保系统的功能正确性，减少潜在的错误和漏洞，从而提高系统的稳定性和性能。OpenComRTOS的开发过程就充分利用了这些优点，以确保其在网络环境中的高效运行和可靠性。在书中，作者们，包括Eric Verhulst、Raymond T. Boute、José Miguel Sampaio Faria、Bernhard H. C. Sputh和Vitaliy Mezhuyev，详细阐述了如何使用形式化方法进行RTOS的设计和实现。他们探讨了如何从需求分析阶段开始，运用形式化技术建立精确的规格说明，然后进行形式验证，以确保这些规格能够满足预期的性能和安全要求。此外，他们还讨论了如何将这些方法应用于网络通信协议栈的设计，以实现高效、实时的网络通信。书中提到的形式化开发流程不仅限于理论，还包括实际的工程实践，这意味着读者可以学习如何将这些技术应用到自己的项目中。这包括使用特定的工具和方法进行模型验证、代码生成和测试，以确保生成的RTOS代码不仅符合规格，而且能够在目标硬件上正确无误地运行。在安全性方面，由于形式化方法的严谨性，OpenComRTOS能够满足如IEC61508这样的工业安全标准，这对于在关键领域应用的嵌入式系统至关重要。这些标准要求软件必须经过严格的分析和验证，以确保在故障发生时能够维持预定的安全等级。总而言之，《Formal Development of a Network-Centric RTOS》提供了一种独特的方法论，结合了形式化方法和网络为中心的视角，为开发高质量、高可靠的实时操作系统提供了全面的指导。这本书对于从事嵌入式系统、实时操作系统和形式化方法研究的工程师和学者来说，是一份宝贵的参考资料。

List of Figures

Fig. 1.1 Uniﬁed Systems Engineering Methodology ......................... 7

Fig. 2.1 The context of systems engineering .................................. 16

Fig. 2.2 Superloop schedule with three interrupt sources .................... 22

Fig. 2.3 Two periodic tasks scheduled with RMA ............................ 24

Fig. 2.4 Three tasks sharing a resource with and without priority

inheritance support .................................................... 30

Fig. 3.1 Example of a speciﬁcation in TLA

................................. 52

Fig. 3.2 Header of the TLA

model .......................................... 56

Fig. 3.3 Bottom of the TLA

Speciﬁcation of Harris’ algorithm ............ 57

Fig. 3.4 Deﬁnition of Coherence .............................................. 57

Fig. 3.5 Deﬁnition of action CreateI .......................................... 57

Fig. 3.6 Deﬁnition of action LocateD ......................................... 58

Fig. 3.7 Deﬁnition of action CasD2 ........................................... 59

Fig. 3.8 Comparison of the formalisms ....................................... 67

Fig. 4.1 Rendezvous in SendReceivePacketService .......................... 83

Fig. 6.1 A simple OpenComRTOS application using Port Hubs............. 108

Fig. 6.2 Hub diagram........................................................... 109

Fig. 6.3 Application diagram with all Interactions for the

Semaphore Loop ...................................................... 115

Fig. 7.1 Task interactions with a Hub ......................................... 124

Fig. 7.2 Asynchronous Task interactions with Hubs ......................... 129

Fig. A.1 Screenshot of OpenVE’s the ‘New Project’ dialogue ............... 144

Fig. A.2 OpenVE with opened Topology View (no nodes deﬁned yet) ...... 145

Fig. A.3 The dialogue to specify the properties of the new win32-node ..... 145

xvi List of Figures

Fig. A.4 Topology view showing the newly created win32-node ............ 146

Fig. A.5 OpenVE Application Diagram with highlighted Task button ....... 146

Fig. A.6 ‘New Task’ dialogue, with highlighted ‘Task

Entrypoint’ creation button ........................................... 147

Fig. A.7 The Task Entrypoint creation dialogue, showing the

source code that will be generated ................................... 147

Fig. A.8 Application diagram showing the newly created Task1 ............. 148

Fig. A.9 Application diagram showing both Task1 and Task2 ............... 149

Fig. A.10 The ‘New Semaphore’ dialogue of OpenVE ........................ 149

Fig. A.11 Application diagram with all entities, showing the

interaction selection menu ............................................ 150

Fig. A.12 Application diagram with all Interactions for the

Semaphore Loop ...................................................... 150

Fig. A.13 Source code for Task1, the incorrectly placed

interactions highlighted ............................................... 151

Fig. A.14 The ‘New stdioHostServer’ dialogue of OpenVE ................... 151

Fig. A.15 Application diagram with the complete Semaphore-

Loop and the Stdio Host Server ...................................... 152

Fig. A.16 Source code of Task1 with Semaphore and Stdio Host

Server Interactions .................................................... 152

Fig. A.17 Console output upon running the ‘SemaphoreLoop’ project ....... 153

Fig. A.18 Edit Link Ports Dialogue, with highlighted ‘Add Link

Port’ button ............................................................ 154

Fig. A.19 OpenVE link conﬁguration dialogue ................................. 154

Fig. A.20 Topology of the two Win32 Nodes connected with a

bidirectional Link ..................................................... 155

Fig. A.21 OpenVE with open ‘Properties’ side-pane and

highlighted ‘node’ property .......................................... 156

Fig. A.22 Console output of both win32-nodes................................. 156

Fig. A.23 OpenVE with open Property Pane ................................... 157

Fig. A.24 Tracing enabled Application Diagram ............................... 159

Fig. A.25 OpenTracer displaying parts of the

SemaphoreTracing_MP_TCPIP example trace ........................ 159

Fig. A.26 Stages of IRQ handling in a typical Microcontroller System ....... 161

Fig. A.27 Screenshot of the Interrupt Latency GUI Application............... 164

Fig. A.28 Interrupt latency measurement system topology .................... 165

Fig. A.29 Interrupt latency measurement system application diagram ........ 166

Fig. A.30 Measured IRQ to ISR Latency on ARM Cortex M3

50MHz (logarithmic scale) ........................................... 167

Fig. A.31 Measured IRQ to Task Latency on ARM Cortex M3

50MHz (logarithmic scale) ........................................... 167

Fig. B.1 Numbers of beans ..................................................... 182

Fig. B.2 Bag of beans........................................................... 183

Fig. B.3 The Bags module from Specifying Systems compressed ............ 185

剩余237页未读，继续阅读

TsiuHinghiok

粉丝: 6
资源: 64

形式化开发网络中心实时操作系统

Formal verification of Real-Time Wireless Sensor Networks protocols Scaling Up

软件测试常用英语词汇

redefinition of formal parameter

How can a function access actual parameter values for those actual parameters that do not correspond to any formal parameter?

Dijkstra算法论文有哪些

redefinition of formal parameter 'm'

def Formal_Img(l): random_number=(ord(l)-ord('a'))*800+random.randint(1,10) formal_img=X_test[random_number] return formal_img def Player_Img(img): formal_img=img player_img=Image.fromarray(formal_img) return player_img

最新资源