Developing Reliable Component-Based Software in Mediator

Yi Li¹⁵

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11232))

Included in the following conference series:

International Conference on Formal Engineering Methods

1145 Accesses

Abstract

Component-based development is widely used to reduce the development cost of complex systems. In this pattern, software features are organized, encapsulated and reused as components. In this report, we present a component-based modeling framework based on the modeling language Mediator that aims to build formally verified software, both on model-level and code-level. This work is the core part of a Ph.D. thesis.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic

$34.99 /Month

Get 10 units per month
Download Article/Chapter or eBook
1 Unit = 1 Article or 1 Chapter
Cancel anytime

Buy Now

Chapter: USD 29.95; Price excludes VAT (USA)

eBook: USD 39.99; Price excludes VAT (USA)

Softcover Book: USD 54.99; Price excludes VAT (USA)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

Abdulla, P.A., Deneux, J., Stålmarck, G., Ågren, H., Åkerlund, O.: Designing safe, reliable systems using scade. In: Margaria, T., Steffen, B. (eds.) ISoLA 2004. LNCS, vol. 4313, pp. 115–129. Springer, Heidelberg (2006). https://doi.org/10.1007/11925040_8
Chapter Google Scholar
Amnell, T., et al.: UPPAAL - now, next, and future. In: Cassez, F., Jard, C., Rozoy, B., Ryan, M.D. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 99–124. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45510-8_4
Chapter Google Scholar
Berry, G., Gonthier, G.: The Esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87–152 (1992)
Article Google Scholar
Cataño, N., Rivera, V.: EventB2Java: a code generator for Event-B. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 166–171. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40648-0_13
Chapter Google Scholar
Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_22
Chapter Google Scholar
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33826-7_16
Chapter Google Scholar
Hahn, B., Valentine, D.T.: SIMULINK toolbox. In: Essential MATLAB for Engineers and Scientists, pp. 341–356. Academic Press (2016)
Google Scholar
Jeannin, J., et al.: Formal verification of ACAS X, an industrial airborne collision avoidance system. In: Proceedings of EMSOFT 2015, pp. 127–136. IEEE (2015)
Google Scholar
Kim, H., Lee, E.A., Broman, D.: A toolkit for construction of authorization service infrastructure for the internet of things. In: Proceedings of IoTDI 2017, pp. 147–158. ACM (2017)
Google Scholar
Klein, G., et al.: seL4: formal verification of an OS kernel. In: Proceedings of SOSP 2009, pp. 207–220. ACM (2009)
Google Scholar
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47
Chapter Google Scholar
Li, Y., Sun, M.: Component-based modeling in mediator. In: Proença, J., Lumpe, M. (eds.) FACS 2017. LNCS, vol. 10487, pp. 1–19. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68034-7_1
Chapter Google Scholar
Li, Y., Sun, M.: Generating arduino C codes from mediator. In: de Boer, F., Bonsangue, M., Rutten, J. (eds.) It’s All About Coordination. LNCS, vol. 10865, pp. 174–188. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90089-6_12
Chapter Google Scholar
Liu, Z., Morisset, C., Stolz, V.: rCOS: theory and tool for component-based model driven development. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 62–80. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11623-0_3
Chapter Google Scholar
Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58–64 (2010)
Article Google Scholar
National Instruments: Labview. http://www.ni.com/zh-cn/shop/labview.html

Download references

Acknowledgements

The work is supervised by Prof. Meng Sun, and partially supported by the National Natural Science Foundation of China under grant no. 61532019, 61202069, 61272160 and 61772038.

Author information

Authors and Affiliations

LMAM and Department of Informatics, School of Mathematical Sciences, Peking University, Beijing, China
Yi Li

Authors

Yi Li
View author publications
You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yi Li .

Editor information

Editors and Affiliations

University of Auckland, Auckland, New Zealand
Jing Sun
Peking University, Beijing, China
Meng Sun

Rights and permissions

Reprints and permissions

Copyright information

About this paper

Cite this paper

Li, Y. (2018). Developing Reliable Component-Based Software in Mediator. In: Sun, J., Sun, M. (eds) Formal Methods and Software Engineering. ICFEM 2018. Lecture Notes in Computer Science(), vol 11232. Springer, Cham. https://doi.org/10.1007/978-3-030-02450-5_29

Download citation

DOI: https://doi.org/10.1007/978-3-030-02450-5_29
Published: 11 October 2018
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02449-9
Online ISBN: 978-3-030-02450-5
eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics