A proof system of the CaIT calculus

doi:10.1007/s11704-022-2258-3

Front. Comput. Sci.

2024, Vol. 18

Issue (2) : 182401 https://doi.org/10.1007/s11704-022-2258-3

Theoretical Computer Science

A proof system of the CaIT calculus

Ningning CHEN, Huibiao ZHU(

)

Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China

Download: PDF(9013 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

The Internet of Things (IoT) can realize the interconnection of people, machines, and things anytime, anywhere. Most of the existing research mainly focuses on the practical applications of IoT, and there is a lack of research on modeling and reasoning about IoT systems from the perspective of formal methods. Thus, the Calculus of the Internet of Things (CaIT) has been proposed to specify and analyze IoT systems before the actual implementation, which can effectively improve development efficiency, and enhance system quality and reliability. To verify the correctness of IoT systems described by CaIT, this paper presents a proof system for CaIT, in which specifications and verifications are based on the extended Hoare Logic with time. Furthermore, we explore the cooperation between isolated proofs to validate the postconditions of the communication actions occurring in these proofs, with a particular focus on broadcast communication. We also demonstrate the soundness of our proof system. A simple “smart home” is given to illustrate the availability of our proof system.

Keywords Internet of Things (IoT) Calculus of the Internet of Things (CaIT) extended hoare logic cooperation smart home

Corresponding Author(s): Huibiao ZHU

Just Accepted Date: 19 December 2022 Issue Date: 23 March 2023

Cite this article:

Ningning CHEN,Huibiao ZHU. A proof system of the CaIT calculus[J]. Front. Comput. Sci., 2024, 18(2): 182401.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-022-2258-3
https://academic.hep.com.cn/fcs/EN/Y2024/V18/I2/182401

$N e t w o r k$
$N, N 1$	$::=$	$0$	Empty network
	$\|$	$N ‖ N 1$	Parallel composition
	$\|$	$N; N 1$	Sequential composition
	$\|$	$(v c ′) N$	Channel restriction
	$\|$	$n [Γ ? B] l u$	Node
$B o d y$
$B, B 1$	$::=$	$B ‖ B 1$	Parallel composition
	$\|$	$P$	Process
	$\|$	$(s ← v 3); B$	Sensor
	$\|$	$(a → v 4); B$	Actuator
$P r o c e s s$
$P, Q$	$::=$	$n i l$	Termination
	$\|$	$s k i p$	Skip
	$\|$	$P ‖ Q$	Parallel composition
	$\|$	$[b] P, Q$	Conditional choice
	$\|$	$! ? v 2 ? b c; P$	Broadcast output
	$\|$	$ρ; P$	Intra-node action
	$\|$	$? π; P ? Q$	Action with timeout
	$\|$	$w h i l e b d o P o d$	Iteration
$ρ$	$::=$	$σ$	Delay
	$\|$	$@ l ~$	Querying location
	$\|$	$s ? y$	Sensor reading
	$\|$	$a! v$	Actuator writing
$π$	$::=$	$c! ? v 1 ?$	Point-to-point output
	$\|$	$c ? (x 1)$	Point-to-point input
	$\|$	$? (x 2) b c$	Broadcast input
	$\|$	$m o v e_l ′$	Migration

Tab.1 The syntax of the CaIT calculus

$N U L L : N ‖ 0 ≡ N$
$N C O M M : N ‖ N ′ ≡ N ′ ‖ N$
$N A S S O C : (N ‖ N ′) ‖ N ″ ≡ N ‖ (N ′ ‖ N ″)$
$N P L I T : n [Γ ? P ‖ Q] l u ≡ n [Γ ? P] l u ‖ n [Γ ? Q] l u$
$C H A N R E ? 1 : (v c) 0 = 0$
$C H A N R E ? 2 : (v c) (v d) N = (v d) (v c) N$
$C H A N R E ? 3 : (v c) (N ‖ N 1) = N ‖ (v c) N 1, i f c n o t i n N 1 .$

Tab.2 The structural equivalence

$C h a n (n [Γ ? B] l u) = C h a n (B),$
$C h a n (B ‖ B 1) = C h a n (B) ∪ C h a n (B 1),$
$C h a n ((s ← v 3); B) = C h a n (B),$
$C h a n ((a → v); B) = C h a n (B),$
$C h a n (n i l) = ?,$
$C h a n (s k i p) = ?,$
$C h a n (P ‖ Q) = C h a n (P) ∪ C h a n (Q),$
$C h a n ([b] P, Q) = C h a n (P) ∪ C h a n (Q),$
$C h a n (! ? v ? b c; P) = {b c} ∪ C h a n (P),$
$C h a n (ρ; P) = C h a n (P), w h e r e ρ ∈ {σ, @ l ~, s ? y, a! v} .$
$C h a n (? π; P ? Q) = C h a n (π) ∪ C h a n (P) ∪ C h a n (Q),$
$w h e r e π ∈ {c! ? v ?, c ? (x), ? (x 2) b c, m o v e_l ′)} .$
$C h a n (c! ? v ?) = {c}, C h a n (c ? (x)) = {c},$
$C h a n (? (x 2) b c) = {b c}, C h a n (m o v e_l ′) = ?,$
$C h a n (w h i l e b d o P o d) = C h a n (P),$
$C h a n (0) = ?,$ $C h a n (N ‖ N 1) = C h a n (N) ∪ C h a n (N 1),$
$C h a n (N; N 1) = C h a n (N) ∪ C h a n (N 1) .$

Tab.3 The definition of function

C h a n

Fig.1 A simple smart home implied from [12]

1	K Ashton . That “internet of things” thing. RFID Journal, 2009, 22(7): 97−114
2	J, Gubbi R, Buyya S, Marusic M Palaniswami . Internet of things (IoT): a vision, architectural elements, and future directions. Future Generation Computer Systems, 2013, 29( 7): 1645–1660
3	Y Zhang . Technology framework of the internet of things and its application. In: Proceedings of 2011 International Conference on Electrical and Control Engineering. 2011, 4109−4112
4	L, Atzori A, Iera G Morabito . The internet of things: a survey. Computer Networks, 2010, 54( 15): 2787–2805
5	M, Hosseinzadeh Q T, Tho S, Ali A M, Rahmani A, Souri M, Norouzi B Huynh . A hybrid service selection and composition model for cloud-edge computing in the internet of things. IEEE Access, 2020, 8: 85939–85949
6	Y, Harbi Z, Aliouat A, Refoufi S Harous . Recent security trends in internet of things: a comprehensive survey. IEEE Access, 2021, 9: 113292–113314
7	K, Nienhuis A, Joannou T, Bauereiss A, Fox M, Roe B, Campbell M, Naylor R M, Norton S W, Moore P G, Neumann I, Stark R N M, Watson P Sewell . Rigorous engineering for hardware security: formal modelling and proof in the CHERI design and implementation process. In: Proceedings of 2020 IEEE Symposium on Security and Privacy. 2020, 1003−1020
8	M, Asavoae I, Haur M, Jan Hedia B, Ben M Schoeberl . Towards formal co-validation of hardware and software timing models of CPSs. In: Proceedings of the 9th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems. 2019, 203−227
9	B Schmidt . Programmnetzlisten: Ein formales Modell fur die Verifikation von Hardwarenaher Software in Eingebetteten Systemen. Technische Universitat Kaiserslautern, Dissertation, 2020
10	I, Lanese L, Bedogni Felice M Di . Internet of things: a process calculus approach. In: Proceedings of the 28th Annual ACM Symposium on Applied Computing. 2013, 1339−1346
11	C, Bodei P, Degano G L, Ferrari L Galletta . Where do your IoT ingredients come from? In: Proceedings of the 18th International Conference on Coordination Languages and Models. 2016, 35–50
12	R, Lanotte M Merro . A semantic theory of the internet of things. Information and Computation, 2018, 259: 72–101
13	K R, Apt E R, Olderog K R Apt . Verification of Sequential and Concurrent Programs. 3rd ed. New York: Springer, 2009
14	J Hooman . Compositional verification of real-time systems using extended Hoare triples. In: Proceedings of the Real-Time: Theory in Practice, REX Workshop. 1991, 252−290
15	J Hooman . Extending Hoare logic to real-time. Formal Aspects of Computing, 1994, 6( S1): 801–825
16	I F, Akyildiz J M, Jornet C Han . Terahertz band: next frontier for wireless communications. Physical Communication, 2014, 12: 16–32
17	der Heijden F, van R P W, Duin Ridder D, De D M J Tax . Classification, Parameter Estimation and State Estimation: an Engineering Approach Using MATLAB. Chichester: John Wiley & Sons, ltd., 2004
18	K V S Prasad . A calculus of broadcasting systems. Science of Computer Programming, 1995, 25(2–3): 2–3
19	S, Nanz C Hankin . A framework for security analysis of mobile wireless networks. Theoretical Computer Science, 2006, 367(1–2): 1–2
20	M Merro . An observational theory for mobile ad hoc networks (full version). Information and Computation, 2009, 207( 2): 194–208
21	C A R Hoare . An axiomatic basis for computer programming. Communications of the ACM, 1969, 12( 10): 576–580
22	G, Barthe M, Gaboardi E J G, Arias J, Hsu C, Kunz P Y Strub . Proving differential privacy in Hoare logic. In: Proceedings of the 27th IEEE Computer Security Foundations Symposium. 2014, 411−424
23	R, Arthan U, Martin P Oliva . A Hoare logic for linear systems. Formal Aspects of Computing, 2013, 25( 3): 345–363
24	C, Luo S, Qin Z Qiu . Verifying BPEL-like programs with Hoare logic. Frontiers of Computer Science in China, 2008, 2( 4): 344–356
25	Boer F S de . A Hoare logic for dynamic networks of asynchronously communicating deterministic processes. Theoretical Computer Science, 2002, 274(1–2): 1–2
26	K R, Apt N, Francez Roever W P de . A proof system for communicating sequential processes. ACM Transactions on Programming Languages and Systems, 1980, 2( 3): 359–385
27	C A R, Hoare J He . Unifying Theories of Programming. London: Prentice Hall, 1998
28	L C Paulson . Isabelle: a Generic Theorem Prover. Berlin: Springer, 1994
29	G, Huet G, Kahn C Paulin-Mohring . The coq proof assistant: a tutorial. Rapport Technique, 1997, 178

[1]

FCS-22258-OF-NC_suppl_1

Download

[1]	Lei CHEN, Mitchell TSENG, Xiang LIAN, . Development of foundation models for Internet of Things[J]. Front. Comput. Sci., 2010, 4(3): 376-385.

Viewed

Full text

Abstract

Cited

Shared

Discussed