Abstract
This paper presents work on object-oriented modelling of wireless biomedical sensors in order to analyse their behaviour. These sensors combine synchronous and asynchronous communication, hard and soft real-time requirements, and have limited resources in terms of memory and energy. Moreover, design decisions tend to influence the validity of other requirements; e.g., higher communication throughput increases energy requirements. A single language is proposed in which design concerns can be expressed and analysed. This language is an extension for real-time systems of Creol, a modelling language specifically designed for distributed, asynchronously communicating, active objects. The extension proposes language primitives to capture requirements on the progress of time and the progress of the system. We integrate the timing requirements and the underlying object-oriented modelling language in a timed denotational semantics. The controller of a biomedical sensor node is used to illustrate the approach, for which there are both hard real-time requirements imposed by taking sensor measurements and soft requirements imposed by the communication network.
This work has been supported by the EU-project IST-33826 CREDO: Modelling and analysis of evolutionary structures for distributed services (http://credo.cwi.nl).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
International Organization for Standardization Geneva: Information technology – Open Distributed Processing – Reference model: Overview. Iso/iec 10746-1:1998 edn (1998)
Graf, S., Hooman, J.: Correct development of embedded systems. In: Oquendo, F., Warboys, B.C., Morrison, R. (eds.) EWSA 2004. LNCS, vol. 3047, pp. 241–249. Springer, Heidelberg (2004)
Oliver, I.: Model driven embedded systems. In: ACSD, vol. 5. IEEE Computer Society Press, Los Alamitos (2003)
SysML Partners: OMG SysML Specification. (March 2007), http://www.sysml.org/specs.htm
Bowen, J.: The ethics of safety-critical systems. Communications of the ACM 43(4), 91–97 (2000)
Johnsen, E.B., Owe, O., Yu, I.C.: Creol: A type-safe object-oriented model for distributed concurrent systems. Theoretical Computer Science 365(1-2), 23–66 (2006)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96, 73–155 (1992)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science 285(2), 187–243 (2002)
Dovland, J., Johnsen, E.B., Owe, O.: Verification of concurrent objects with asynchronous method calls. In: SwSTE, pp. 141–150. IEEE Computer Society Press, Los Alamitos (2005)
Ábrahám-Mumm, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: Verification for java’s reentrant multithreading concept. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, p. 5. Springer, Heidelberg (2002)
Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Software and Systems Modeling 6(1), 35–58 (2007)
Hoare, C.A.R.: Monitors: An operating system structuring concept. Communications of the ACM 17(10), 549–557 (1974)
Johnsen, E.B., Owe, O., Arnestad, M.: Combining active and reactive behavior in concurrent objects. In: Langmyhr, D. (ed.) NIK, November 2003, pp. 193–204. Tapir Academic Publisher (2003)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Hooman, J.: Extending Hoare logic to real-time. Formal Aspects of Computing 6(6A), 801–825 (1994)
Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Lazy behavioral subtyping. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 52–67. Springer, Heidelberg (2008)
de Boer, F.S., Kok, J.N., Palamidessi, C., Rutten, J.J.M.M.: The failure of failures in a paradigm for asynchronous communication. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 111–126. Springer, Heidelberg (1991)
Liu, J.W.: Real-Time Systems. Prentice Hall, Upper Saddle River (2000)
Shannon, C.E.: Communication in the presence of noise. Proceedings of the Institute of Radio Engineers 37(1), 10–21 (1949)
Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and precise WCET determination for a real-life processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 469–485. Springer, Heidelberg (2001)
Turski, W.M.: Time considered irrelevant for real-time systems. BIT 28(3), 473–486 (1988)
Mikhajlov, L., Sekerinski, E.: A study of the fragile base class problem. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 355–382. Springer, Heidelberg (1998)
Matsuoka, S., Yonezawa, A.: Analysis of inheritance anomaly in object-oriented concurrent programming languages. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 107–150. MIT Press, Cambridge (1993)
Aksit, M., Bosch, J., van der Sterren, W., Bergmans, L.: Real-time specification inheritance anomalies and real-time filters. In: Tokoro, M., Pareschi, R. (eds.) ECOOP 1994. LNCS, vol. 821, pp. 386–407. Springer, Heidelberg (1994)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal — a tool suite for automatic verification of real–time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)
Tschirner, S., Xuedong, L., Yi, W.: Model-based validation of QoS properties of biomedical sensor networks. In: de Alfaro, L., Palsberg, J. (eds.) EMSOFT, pp. 69–78. ACM Press, New York (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kyas, M., Johnsen, E.B. (2009). A Real-Time Extension of Creol for Modelling Biomedical Sensors. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds) Formal Methods for Components and Objects. FMCO 2008. Lecture Notes in Computer Science, vol 5751. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04167-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-04167-9_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04166-2
Online ISBN: 978-3-642-04167-9
eBook Packages: Computer ScienceComputer Science (R0)