Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
SICS Software-Intensive Cyber-Physical Systems
Erschienen in: SICS Software-Intensive Cyber-Physical Systems 4/2013

01.11.2013 | Special Issue Paper

From software verification to ‘everyware’ verification

verfasst von: Marta Kwiatkowska

Erschienen in: SICS Software-Intensive Cyber-Physical Systems | Ausgabe 4/2013

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Ubiquitous computing is a vision of computing in which the computer disappears from view and becomes embedded in our environment, in the equipment we use, in our clothes, and even in our body. Everyday objects—called ‘everyware’ by Adam Greenfield—are now endowed with sensing, controlled by software, and often wirelessly connected and Internet-enabled. Our increasing dependence on ubiquitous computing creates an urgent need for modelling and verification technologies to support the design process, and hence improve the reliability and reduce production costs. At the same time, the challenges posed by ubiquitous computing are unique, deriving from the need to consider coordination of communities of ‘everyware’ and control physical processes such as drug delivery.
Model-based design and verification techniques have pro-ved useful in supporting the design process by detecting and correcting flaws in a number of ubiquitous computing applications, but are limited by poor scalability, efficiency and range of scenarios that can be handled. In this paper we describe the objectives and initial progress of the research aimed at extending the capabilities of quantitative, probabilistic verification to challenging ubiquitous computing scenarios. The focus is on a advancing quantitative verification in new and previously unexplored directions, including game-based techniques, incorporation of continuous dynamics in addition to stochasticity, and online approaches. The research involves investigating the fundamentals of quantitative verification, development of algorithms and prototype implementations, and experimenting with case studies.
Vorheriger Artikel Supporting incremental behaviour model elaboration
Nächster Artikel Requirements-driven software evolution

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Computer Science - Research and Development

Computer Science – Research and Development (CSRD), formerly Informatik – Forschung und Entwicklung (IFE), is a quarterly international journal that publishes high-quality research and survey papers from the Software Engineering & Systems area.

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Weitere Produktempfehlungen anzeigen
Literatur
1.
Aldini A, Bogliolo A (2012) Model checking of trust-based user-centric cooperative networks. In: AFIN 2012, the fourth international conference on advances in future Internet. ISBN 978-1-61208-211-0
2.
3.
4.
Amnell T, Behrmann G, Bengtsson J, D’Argenio PR, David A, Fehnker A, Hune T, Jeannet B, Larsen KG, Möller MO, Pettersson P, Weise C, Yi W (2001) Uppaal—now, next, and future. In: Cassez F, Jard C, Rozoy B, Ryan M (eds) Modelling and verification of parallel processes. Lecture notes in computer science tutorial, vol 2067. Springer, Berlin, pp 100–125
5.
Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge MATH
6.
Baier C, Haverkort B, Hermanns H, Katoen J-P (2003) Model-checking algorithms for continuous-time Markov chains. IEEE Trans Softw Eng 29:524–541 CrossRef
7.
Baier C, Ciesinski F, Grosser M (2005) Probmela and verification of Markov decision processes. ACM SIGMETRICS Perform Eval Rev 32(4):22–27 CrossRef
8.
Bianco A, de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: Thiagarajan P (ed) Proc FSTTCS’95. LNCS, vol 1026. Springer, Berlin, pp 499–513
9.
Bucur D, Kwiatkowska M (2011) On software verification for TinyOS. J Syst Softw 84(10):1693–1707 CrossRef
10.
Calinescu R, Grunske L, Kwiatkowska M, Mirandola R, Tamburrelli G (2011) Dynamic QoS management and optimisation in service-based systems. IEEE Trans Softw Eng 37(3):387–409 CrossRef
11.
Calinescu R, Ghezzi C, Kwiatkowska M, Mirandola R (2012) Self-adaptive software needs quantitative verification at runtime. Commun ACM 55(9):69–77 CrossRef
12.
Cardelli L (2009) Strand algebras for DNA computing. In: Deaton RJ, Suyama A (eds) DNA. Lecture notes in computer science, vol 5877. Springer, Berlin, pp 12–24
13.
Cassez F, Jessen J, Larsen K, Raskin J-F, Reynier P-A (2009) Automatic synthesis of robust and optimal controllers—an industrial case study. In: Majumdar R, Tabuada P (eds) Hybrid systems: computation and control. Lecture notes in computer science, vol 5469. Springer, Berlin, pp 90–104 CrossRef
14.
15.
Chatterjee K, Henzinger TA (2011) A survey of stochastic omega-regular games. J Comput Syst Sci
16.
Chatterjee K, de Alfaro L, Henzinger T (2006) The complexity of quantitative concurrent parity games. In: Proc SODA’06. ACM, New York, pp 678–687
17.
Chatterjee K, Doyen L, Henzinger TA (2010) Quantitative languages. ACM Trans Comput Log 11(4)
18.
Chen T, Diciolla M, Kwiatkowska M, Mereacre A (2011) Time-bounded verification of CTMCs against real time specifications. In: Proc 8th international conference, formal modeling and analysis of timed systems. LNCS, vol 6919. Springer, Berlin, pp 26–42 CrossRef
19.
Chen T, Chilton C, Jonsson B, Kwiatkowska M (2012) A Compositional Specification Theory for Component Behaviours. In: Seidl H (ed) Proc ESOP’12. Lecture notes in computer science, vol 7211. Springer, Berlin, pp 148–168
20.
Chen T, Diciolla M, Kwiatkowska M, Mereacre A (2012) Quantitative verification of implantable cardiac pacemakers. In: Proc 33rd IEEE real-time systems symposium (RTSS). doi:10.​1109/​RTSS.​2012.​77
21.
Chen T, Diciolla M, Kwiatkowska MZ, Mereacre A (2012) Verification of linear duration properties over continuous-time Markov chains. In: Dang T, Mitchell IM (eds) Proc HSCC. ACM, New York, pp 265–274 CrossRef
22.
Chen T, Forejt V, Kwiatkowska M, Parker D, Simaitis A (2012) Automatic verification of competitive stochastic systems. In: Proc 18th international conference on tools and algorithms for the construction and analysis of systems (TACAS’12). LNCS, vol 7214. Springer, Berlin, pp 315–330 CrossRef
23.
Cheung L, Lynch N, Segala R, Vaandrager F (2004) Switched probabilistic I/O automata. In: Proc 1st international colloquium on theoretical aspects of computing (ICTAC’04). LNCS, vol 3407. Springer, Berlin, pp 494–510 CrossRef
24.
Chilton C, Kwiatkowska M, Wang X (2012) Revisiting timed specification theories: a linear-time perspective. In: Jurdzinski M, Nickovic D (eds) Proc FORMATS’12. Lecture notes in computer science, vol 7595. Springer, Berlin, pp 75–90
25.
Clarke E, Long D, McMillan K (1989) Compositional model checking. In: Proc 4th annual symposium on logic in computer science. IEEE Press, New York, pp 353–362 CrossRef
26.
Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Emerson EA, Sistla AP (eds) Proc CAV. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 154–169
27.
Clarke EM, Grumberg O, Peled DA (2000) Model checking. MIT Press, Cambridge
28.
Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Jensen K, Podelski A (eds) Proc TACAS 2004. Lecture notes in computer science, vol 2988. Springer, Berlin, pp 168–176
29.
Clifford GD, Nemati S, Sameni R (2010) An artificial vector model for generating abnormal electrocardiographic rhythms. Physiol Meas 31(5):595 CrossRef
30.
31.
Crow J, Rushby J (1991) Model-based reconfiguration: toward an integration with diagnosis. In: Proceedings, AAAI-91 (Volume 2), pp 836–841
32.
de Alfaro L, Henzinger TA (2001) Interface automata. Softw Eng Notes 26(5):109–120 CrossRef
33.
de Alfaro L, Henzinger TA (2001) Interface automata. In: Proc 9th FSE, ESEC/FSE-9. ACM, New York, pp 109–120
34.
de Alfaro L, Henzinger T, Jhala R (2001) Compositional methods for probabilistic systems. In: Larsen K, Nielsen M (eds) Proc CONCUR’01. LNCS, vol 2154. Springer, Berlin, pp 351–365
35.
Duflot M, Kwiatkowska M, Norman G, Parker D (2006) A formal analysis of bluetooth device discovery. Int J Softw Tools Technol Transf 8(6):621–632 CrossRef
36.
Eker J, Janneck JW, Lee EA, Liu J, Liu X, Ludvig J, Neuendorffer S, Sachs S, Xiong Y (2003) Taming heterogeneity—the Ptolemy approach. In: Proceedings of the IEEE, pp 127–144
37.
Etessami K, Kwiatkowska M, Vardi M, Yannakakis M (2007) Multi-objective model checking of Markov decision processes. In: Grumberg O, Huth M (eds) Proc TACAS’07. LNCS, vol 4424. Springer, Berlin, pp 50–65
38.
Feng L, Kwiatkowska M, Parker D (2010) Compositional verification of probabilistic systems using learning. In: Proc 7th international conference on quantitative evaluation of SysTems (QEST’10). IEEE Comput Soc, Los Alamitos, pp 133–142 CrossRef
39.
Feng L, Kwiatkowska M, Parker D (2011) Automated learning of probabilistic assumptions for compositional reasoning. In: Giannakopoulou D, Orejas F (eds) Proc FASE’11. LNCS, vol 6603. Springer, Berlin, pp 2–17
40.
Filieri A, Ghezzi C, Tamburrelli G (2011) Run-time efficient probabilistic model checking. In: Taylor RN, Gall H, Medvidovic N (eds) ICSE. ACM, New York, pp 341–350
41.
Forejt V, Kwiatkowska M, Norman G, Parker D (2011) Automated verification techniques for probabilistic systems. In: Bernardo M, Issarny V (eds) Formal methods for eternal networked software systems (SFM’11). LNCS, vol 6659. Springer, Berlin, pp 53–113 CrossRef
42.
Forejt V, Kwiatkowska M, Norman G, Parker D, Qu H (2011) Quantitative multi-objective verification for probabilistic systems. In: Abdulla P, Leino K (eds) Proc TACAS’11. LNCS, vol 6605. Springer, Berlin, pp 112–127
43.
Forejt V, Kwiatkowska M, Parker D (2012) Pareto curves for probabilistic model checking. In: Chakraborty S, Mukund M (eds) Proc ATVA’12. LNCS, vol 7561. Springer, Berlin. doi:10.​1007/​978-3-642-33386-6_​25
44.
Forejt V, Kwiatkowska M, Parker D, Qu H, Ujma M (2012) Incremental runtime verification of probabilistic systems. In: Proc 3rd international conference on runtime verification (RV’12). LNCS Springer, Berlin. doi:10.​1007/​978-3-642-35632-2_​30
45.
Frehse G (2005) PHAVer: algorithmic verification of hybrid systems past HyTech. Springer, Berlin, pp 258–273
46.
Gallina L, Han T, Kwiatkowska M, Marin A, Rossi S, Spano A (2012) Automatic energy-aware performance analysis of mobile ad-hoc networks. In: Proc IFIP Wireless Days (WD’12). doi10.​1109/​WD.​2012.​6402864
47.
Gomes AO, Oliveira MV (2009) Formal specification of a cardiac pacing system. In: Proceedings of the 2nd world Congress on formal methods, FM’09. Springer, Berlin, pp 692–707
48.
Greenfield A (2006) In: Everyware: the dawning age of ubiquitous computing, New Riders
49.
Hahn EM, Han T, Zhang L (2011) Synthesis for PCTL in parametric Markov decision processes. In: Proc 3rd NASA formal methods symposium (NFM’11). LNCS, vol 6617. Springer, Berlin
50.
Hahn EM, Norman G, Parker D, Wachter B, Zhang L (2011) Game-based abstraction and controller synthesis for probabilistic hybrid systems. In: Proc 8th international conference on quantitative evaluation of SysTems (QEST’11). IEEE Comput Soc, Los Alamitos, pp 69–78 CrossRef
51.
Hahn E, Hartmanns A, Hermanns H, Katoen J-P (2012) A compositional modelling and analysis framework for stochastic hybrid systems. Form Methods Syst Des. doi:10.​1007/​s10703-012-0167-z
52.
53.
Heath J, Kwiatkowska M, Norman G, Parker D, Tymchyshyn O (2008) Probabilistic model checking of complex biological pathways. Theor Comput Sci 319(3):239–257 MathSciNetCrossRef
54.
Henzinger TA (1996) The theory of hybrid automata. In: Proceedings of the 11th annual IEEE symposium on logic in computer science, LICS’96. IEEE Comput Soc, Los Alamitos, p 278 CrossRef
55.
Henzinger TA, Sifakis J (2007) The discipline of embedded systems design. Computer 40:32–40 CrossRef
56.
Hillston J (1996) A compositional approach to performance modelling. Cambridge University Press, Cambridge CrossRef
57.
58.
Jiang Z, Pajic M, Connolly A, Dixit S, Mangharam R (2010) Real-time heart model for implantable cardiac device validation and verification. In: ECRTS. IEEE Comput Soc, Los Alamitos, pp 239–248
59.
Jiang Z, Pajic M, Moarref S, Alur R, Mangharam R (2012) Modeling and verification of a dual chamber implantable pacemaker. In: Flanagan C, König B (eds) TACAS. Lecture notes in computer science, vol 7214. Springer, Berlin, pp 188–203
60.
Jones C, O’Hearn P, Woodcock J (2006) Verified software: a grand challenge. Computer 39:93–95 CrossRef
61.
Katoen J-P, Khattri M, Zapreev IS (2005) A Markov reward model checker. In: Quantitative evaluation of systems (QEST). IEEE Comput Soc, Los Alamos, pp 243–244
62.
Kattenbelt M, Kwiatkowska M, Norman G, Parker D (2009) Abstraction refinement for probabilistic software. In: Jones N, Muller-Olm M (eds) Proc VMCAI’09. LNCS, vol 5403. Springer, Berlin, pp 182–197
63.
Kattenbelt M, Kwiatkowska M, Norman G, Parker D (2010) A game-based abstraction-refinement framework for Markov decision processes. Form Methods Syst Des 36(3):246–280 CrossRefMATH
64.
Kroeker KL (2011) The rise of molecular machines. Commun ACM 54(12):11–13 CrossRef
65.
Kwiatkowska M (2007) Quantitative verification: models, techniques and tools. In: Proc ESEC/FSE’07. ACM, New York, pp 449–458
66.
Kwiatkowska M, Norman G, Segala R, Sproston J (2002) Automatic verification of real-time systems with discrete probability distributions. Theor Comput Sci 282:101–150 MathSciNetCrossRefMATH
67.
Kwiatkowska M, Norman G, Parker D, Sproston J (2006) Performance analysis of probabilistic timed automata using digital clocks. Form Methods Syst Des 29:33–78 CrossRefMATH
68.
Kwiatkowska M, Norman G, Parker D (2007) Stochastic model checking. In: Bernardo M, Hillston J (eds) Formal methods for the design of computer, communication and software systems: performance evaluation (SFM’07). LNCS (Tutorial volume), vol 4486. Springer, Berlin, pp 220–270 CrossRef
69.
Kwiatkowska M, Norman G, Parker D, Sproston J (2008) Modeling and verification of real-time systems: formalisms and software tools, chapter verification of real-time probabilistic systems Wiley, New York, pp 249–288 CrossRef
70.
Kwiatkowska M, Rodden T, Sassone V (eds) (2008) From computers to ubiquitous computing, by 2020, vol 366. Royal Soc, London. Discussion Meeting Issue
71.
Kwiatkowska M, Norman G, Parker D (2010) A framework for verification of software with time and probabilities. In: Chatterjee K, Henzinger T (eds) Proc FORMATS’10. LNCS, vol 6246. Springer, Berlin, pp 25–45
72.
Kwiatkowska M, Norman G, Parker D (2010) Symbolic systems biology, chapter probabilistic model checking for systems biology Jones & Bartlett, Boston, pp 31–59
73.
Kwiatkowska M, Norman G, Parker D, Qu H (2010) Assume-guarantee verification for probabilistic systems. In: Esparza J, Majumdar R (eds) Proc TACAS’10. LNCS, vol 6105. Springer, Berlin, pp 23–37
74.
Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Proc CAV’11. LNCS, vol 6806. Springer, Berlin, pp 585–591
75.
Kwiatkowska M, Parker D, Qu H (2011) Incremental quantitative verification for Markov decision processes. In: Proc IEEE/IFIP international conference on dependable systems and networks (DSN-PDS’11). IEEE Comput Soc, Los Alamitos, pp 359–370 CrossRef
76.
Lakin M, Parker D, Cardelli L, Kwiatkowska M, Phillips A (2012) Design and analysis of DNA strand displacement devices using probabilistic model checking. J R Soc Interface 9(72):1470–1485 CrossRef
77.
Larsen KG, Nyman U, Wasowski A (2006) Interface input/output automata. In: FM 2006. LNCS series. Springer, Berlin
78.
Lutz RR, Lutz JH, Lathrop JI, Klinge T, Henderson E, Mathur D, Sheasha DA (2012) Engineering and verifying requirements for programmable self-assembling nanomachines. In: ICSE. IEEE Press, New York, pp 1361–1364
79.
MacKenzie A, Wicker SB (2003) Stability of multipacket slotted aloha with selfish users and perfect information. In: INFOCOM
80.
McMillan KL (2000) A methodology for hardware verification using compositional model checking. Sci Comput Program 37(1–3):279–309 CrossRefMATH
81.
McSharry P, Clifford G, Tarassenko L, Smith L (2003) A dynamical model for generating synthetic electrocardiogram signals. IEEE Trans Biomed Eng 50(3):289–294 CrossRef
82.
Milner R (2006) Ubiquitous computing: shall we understand it? Comput J 49(4):383–389 CrossRef
83.
84.
Norman G, Palamidessi C, Parker D, Wu P (2009) Model checking probabilistic and stochastic extensions of the pi-calculus. IEEE Trans Softw Eng 35(2):209–223 CrossRef
85.
Palamidessi C, Herescu OM (2005) A randomized encoding of the pi-calculus with mixed choice. Theor Comput Sci 335(2–3):373–404 MathSciNetCrossRefMATH
86.
Pasareanu CS, Giannakopoulou D, Bobaru MG, Cobleigh JM, Barringer H (2008) Learning to divide and conquer: applying the l* algorithm to automate assume-guarantee reasoning. Form Methods Syst Des 32(3):175–205 CrossRefMATH
87.
Phillips A, Cardelli L (2009) A programming language for composable DNA circuits. J R Soc Interface
88.
Pnueli A (1985) Logics and models of concurrent systems. chapter in transition from global to modular temporal reasoning about programs. Springer, Berlin, pp 123–144 CrossRef
89.
90.
Qian L, Winfree E (2011) Scaling up digital circuit computation with dna strand displacement cascades. Science 332(6034):1196–1201 CrossRef
91.
Sankaranarayanan S, Fainekos G (2012) Simulating insulin infusion pump risks by in-silico modeling of the insulin-glucose regulatory system. In: Proc CMSB’12. LNCS Springer, Berlin. doi:10.​1007/​978-3-642-33636-2_​19
92.
Sarma S, Brock D, Ashton K (1999) The networked physical world. Technical report, MIT-AUTOID-WH-0001
93.
Segala R (1995) Modelling and Verification of Randomized Distributed Real Time Systems. PhD thesis, Massachusetts Institute of Technology
94.
Sproston J (2000) Decidable model checking of probabilistic hybrid automata. In: Joseph M (ed) FTRTFT. Lecture notes in computer science, vol 1926. Springer, Berlin, pp 31–45
95.
Stoller S, Bartocci E, Seyster J, Grosu R, Havelund K, Smolka S, Zadok E (2012) Runtime verification with state estimation. In: Khurshid S, Sen K (eds) Runtime verification. Lecture notes in computer science, vol 7186. Springer, Berlin, pp 193–207 CrossRef
96.
97.
Vardi MY (1985) Automatic verification of probabilistic concurrent finite state programs. In: IEEE annual symposium on foundations of computer science, pp 327–338
98.
99.
Visser W, Havelund K, Brat GP, Park S, Lerda F (2003) Model checking programs. Autom Softw Eng 10(2):203–232 CrossRef
100.
Weiser M (1999) The computer for the 21st century. Mob Comput Commun Rev 3(3):3–11 CrossRef
101.
Wooldridge M (1999) Intelligent agents. In: Weiss G (ed) Multi-agent systems. MIT Press, Cambridge
102.
Yabandeh M, Knezevic N, Kostic D, Kuncak V (2009) Crystalball: predicting and preventing inconsistencies in deployed distributed systems. In: Proceedings of the 6th USENIX symposium on networked systems design and implementation, NSDI’09. USENIX Association, Berkeley, pp 229–244
103.
Younes H, Simmons R (2002) Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma E, Larsen K (eds) Computer aided verification. Lecture notes in computer science, vol 2404. Springer, Berlin, pp 23–39 CrossRef
104.
Yurke B, Turberfield A, Mills A, Simmel F, Neumann J (2000) A DNA-fuelled molecular machine made of dna. Nature 406(6796):605–608 CrossRef
Metadaten
Titel
From software verification to ‘everyware’ verification
verfasst von
Marta Kwiatkowska
Publikationsdatum
01.11.2013
Verlag
Springer Berlin Heidelberg
Erschienen in
SICS Software-Intensive Cyber-Physical Systems / Ausgabe 4/2013
Print ISSN: 2524-8510
Elektronische ISSN: 2524-8529
DOI
https://doi.org/10.1007/s00450-013-0249-1

Weitere Artikel der Ausgabe 4/2013

SICS Software-Intensive Cyber-Physical Systems 4/2013 Zur Ausgabe

Editorial

ERC grants

Special Issue Paper

Supporting incremental behaviour model elaboration

Special Issue Paper

Requirements-driven software evolution

Special Issue Paper

Quantitative reactive modeling and verification

Editorial

Rigorous software engineering

Special Issue Paper

A journey through SMScom: self-managing situational computing

Premium Partner

    Bildnachweise