안전 특성
Safety property분산 컴퓨팅에서 안전 속성은 비공식적으로 분산 시스템 [1][2]또는 분산 알고리즘에서 "어떤 나쁜 일도 일어나지 않습니다"를 요구합니다.데이터베이스 시스템에서 null 필드를 사용하여 데이터를 반환하지 않겠다는 약속은 안전 [3]보장의 한 예입니다.또 다른 예로는 데드록 프리덤이 있습니다.다른 프로세스로부터의 액션을 대기하고 [4]있기 때문에 모든 프로세스 또는 분산 시스템이 속행할 수 없게 되는 일은 없습니다.
안전 속성은 활성 [4]특성과 함께 모델 확인 영역에서 연구되는 선형 시간 특성 유형입니다.라이브 속성과는 달리 안전 속성을 위반하면 위반을 나타내는 유한 실행이 항상 존재합니다.모든 특성은 안전성과 생명체의 [3]교점으로 표현될 수 있다.
레퍼런스
- ^ Rodrigues, Christian Cachin; Rachid Guerraoui; Luís (2010). Introduction to reliable and secure distributed programming (2. ed.). Berlin: Springer Berlin. pp. 22–24. ISBN 978-3-642-15259-7.
- ^ Lamport, L. (1977). "Proving the Correctness of Multiprocess Programs". IEEE Transactions on Software Engineering (2): 125–143. CiteSeerX 10.1.1.137.9454. doi:10.1109/TSE.1977.229904. S2CID 9985552.
- ^ a b Alpern, B.; Schneider, F. B. (1987). "Recognizing safety and liveness". Distributed Computing. 2 (3): 117. CiteSeerX 10.1.1.20.5470. doi:10.1007/BF01782772. S2CID 9717112.
- ^ a b Baier, Christel; Katoen, Joost-Pieter (2008). Principles of Model Checking. MIT Press. p. 104. ISBN 9780262026499.