Safety and liveness properties
একটি কম্পিউটার প্রোগ্রামের সম্পাদনার বৈশিষ্ট্যগুলি-বিশেষত সমবর্তী এবং বিতরণকৃত সিস্টেমগুলির জন্য-দীর্ঘদিন ধরে সুরক্ষা বৈশিষ্ট্য ("খারাপ জিনিস ঘটে না") এবং প্রাণবন্ত বৈশিষ্ট্য ("ভাল জিনিস ঘটে") দিয়ে প্রণয়ন করা হয়েছে। একটি সহজ উদাহরণ নিরাপত্তা এবং প্রাণবন্ততা ব্যাখ্যা করবে। পূর্বশর্ত এবং পরবর্তী শর্তের ক্ষেত্রে একটি কর্মসূচি সম্পূর্ণ সঠিক, যদি সন্তোষজনক অবস্থায় শুরু হওয়া কোনও কর্মসূচি সন্তোষজনক অবস্থায় শেষ হয়। সম্পূর্ণ নির্ভুলতা হল একটি নিরাপত্তা সম্পত্তি এবং একটি জীবন্ত সম্পত্তির সংমিশ্রণঃ নিরাপত্তা সম্পত্তি এই "খারাপ জিনিসগুলিকে" নিষিদ্ধ করেঃ এমন মৃত্যুদণ্ড যা সন্তোষজনক অবস্থায় শুরু হয় এবং চূড়ান্ত অবস্থায় শেষ হয় যা সন্তুষ্ট করে না। একটি প্রোগ্রামের জন্য, এই নিরাপত্তা বৈশিষ্ট্যটি সাধারণত হোয়ার ট্রিপল ব্যবহার করে লেখা হয়। প্রাণবন্ত বৈশিষ্ট্য, "ভাল জিনিস" হল যে কার্যকরকরণ সন্তোষজনক অবস্থায় শুরু হয় তা শেষ হয়। মনে রাখবেন যে একটি খারাপ জিনিস বিচ্ছিন্ন, কারণ এটি কার্যকর করার সময় একটি নির্দিষ্ট জায়গায় ঘটে। একটি "ভাল জিনিস" পৃথক হওয়ার দরকার নেই, তবে সমাপ্তির জীবন্ত বৈশিষ্ট্যটি পৃথক। সুরক্ষা বৈশিষ্ট্য এবং প্রাণবন্ত বৈশিষ্ট্যের জন্য শেষ পর্যন্ত প্রস্তাবিত আনুষ্ঠানিক সংজ্ঞাগুলি দেখায় যে এই পচন কেবল স্বজ্ঞাতভাবে আকর্ষণীয়ই নয়, সম্পূর্ণওঃ একটি কার্যকরকরণের সমস্ত বৈশিষ্ট্য নিরাপত্তা এবং প্রাণবন্ত বৈশিষ্ট্যের সংমিশ্রণ। উপরন্তু, পচন ঘটানো সহায়ক হতে পারে, কারণ আনুষ্ঠানিক সংজ্ঞাগুলি একটি প্রমাণ সক্ষম করে যে সুরক্ষা বৈশিষ্ট্য যাচাই করার জন্য বনাম জীবন্ত বৈশিষ্ট্য যাচাই করার জন্য বিভিন্ন পদ্ধতি ব্যবহার করা আবশ্যক। নিরাপত্তা একটি নিরাপত্তা সম্পত্তি মৃত্যুদণ্ড কার্যকর করার সময় বিচ্ছিন্ন খারাপ জিনিস ঘটতে নিষেধ করে। একটি নিরাপত্তা সম্পত্তি এইভাবে যা নিষিদ্ধ তা উল্লেখ করে যা অনুমোদিত তা চিহ্নিত করে। খারাপ জিনিসটি বিচ্ছিন্ন হওয়ার প্রয়োজনীয়তার অর্থ হল মৃত্যুদন্ড কার্যকর করার সময় ঘটে যাওয়া একটি খারাপ জিনিস অবশ্যই কিছু সনাক্তযোগ্য বিন্দুতে ঘটে। একটি পৃথক খারাপ জিনিসের উদাহরণ যা একটি নিরাপত্তা বৈশিষ্ট্য সংজ্ঞায়িত করতে ব্যবহার করা যেতে পারে তার মধ্যে রয়েছেঃ একটি কার্যকরকরণ যা একটি প্রদত্ত পূর্বশর্ত পূরণকারী অবস্থায় শুরু হয় তা শেষ হয়, কিন্তু চূড়ান্ত অবস্থা প্রয়োজনীয় পোস্ট শর্ত পূরণ করে না; দুটি সমবর্তী প্রক্রিয়ার একটি কার্যকরকরণ, যেখানে উভয় প্রক্রিয়ার জন্য প্রোগ্রাম কাউন্টারগুলি একটি সমালোচনামূলক বিভাগের মধ্যে বিবৃতি নির্ধারণ করে; দুটি সমবর্তী প্রক্রিয়াগুলির একটি কার্যকরকরণ যেখানে প্রতিটি প্রক্রিয়া অন্যটির অবস্থা পরিবর্তনের জন্য অপেক্ষা করছে (অচলাবস্থা হিসাবে পরিচিত)। একটি প্রোগ্রামের এক্সিকিউশনকে আনুষ্ঠানিকভাবে বর্ণনা করা যেতে পারে প্রোগ্রামের অসীম ক্রম দিয়ে বলা হয় যে এক্সিকিউশন এগিয়ে যাওয়ার ফলস্বরূপ, যেখানে একটি সমাপ্তি প্রোগ্রামের শেষ অবস্থা অসীমভাবে পুনরাবৃত্তি করা হয়। আগ্রহের একটি প্রোগ্রামের জন্য, আসুন সম্ভাব্য প্রোগ্রাম অবস্থার সেটকে নির্দেশ করি, প্রোগ্রাম অবস্থার সীমাবদ্ধ ক্রমের সেটকে নির্দেশ করি এবং প্রোগ্রাম অবস্থার অসীম ক্রমের সেটকে নির্দেশ করি। সম্পর্কটি অনুক্রমের জন্য ধারণ করে এবং আই. এফ. এফ একটি উপসর্গ বা সমান। একটি প্রোগ্রামের বৈশিষ্ট্য হল অনুমোদিত মৃত্যুদণ্ডের সেট। একটি নিরাপত্তা সম্পত্তির অপরিহার্য বৈশিষ্ট্য হলঃ যদি কিছু সম্পাদন সন্তুষ্ট না হয় তবে সেই নিরাপত্তা সম্পত্তির জন্য সংজ্ঞায়িত খারাপ জিনিসটি কোনও সময়ে ঘটে। লক্ষ্য করুন যে এই ধরনের একটি খারাপ জিনিসের পরে, যদি আরও কার্যকর করার ফলে একটি মৃত্যুদন্ড কার্যকর হয়, তবে এটিও সন্তুষ্ট করে না, কারণ খারাপ জিনিসটিও ঘটে। আমরা খারাপ জিনিসগুলির অপরিবর্তনীয়তার বিষয়ে এই অনুমানটিকে একটি নিরাপত্তা সম্পত্তি হিসাবে সংজ্ঞায়িত বৈশিষ্ট্য হিসাবে গ্রহণ করি। ভবিষ্যদ্বাণী যুক্তিতে এটিকে আনুষ্ঠানিক করা একটি নিরাপত্তা সম্পত্তি হওয়ার জন্য একটি আনুষ্ঠানিক সংজ্ঞা দেয়। সুরক্ষা বৈশিষ্ট্যগুলির জন্য এই আনুষ্ঠানিক সংজ্ঞাটি বোঝায় যে যদি কোনও কার্যকরকরণ কোনও সুরক্ষা বৈশিষ্ট্যকে সন্তুষ্ট করে তবে প্রতিটি উপসর্গ (শেষ অবস্থার পুনরাবৃত্তি সহ) সন্তুষ্ট হয়। জীবন্ততা একটি জীবন্ত বৈশিষ্ট্য প্রতিটি কার্যকরকরণের জন্য ভাল জিনিস নির্ধারণ করে বা সমতুল্যভাবে এমন কিছু বর্ণনা করে যা কার্যকরকরণের সময় অবশ্যই ঘটতে হবে। ভাল জিনিসটি বিচ্ছিন্ন হওয়ার দরকার নেই-এতে অসীম সংখ্যক পদক্ষেপ জড়িত থাকতে পারে। জীবন্ত বৈশিষ্ট্য সংজ্ঞায়িত করতে ব্যবহৃত একটি ভাল জিনিসের উদাহরণগুলির মধ্যে রয়েছেঃ উপযুক্ত অবস্থায় শুরু হওয়া একটি কার্যকরকরণের সমাপ্তি; উপযুক্ত অবস্থায় শুরু হওয়া একটি কার্যকরকরণের সমাপ্তি না করা; যখনই প্রবেশের চেষ্টা করা হয় তখন একটি সমালোচনামূলক বিভাগে শেষ পর্যন্ত প্রবেশের নিশ্চয়তা দেওয়া হয়; বিতর্কের উপস্থিতিতে কোনও সম্পদে ন্যায্য প্রবেশাধিকার। প্রথম উদাহরণে ভাল জিনিসটি বিচ্ছিন্ন তবে অন্যদের মধ্যে নয়। একটি নির্দিষ্ট রিয়েল-টাইম বাউন্ডের মধ্যে একটি উত্তর তৈরি করা একটি লাইভনেস সম্পত্তির পরিবর্তে একটি সুরক্ষা সম্পত্তি। এর কারণ হল একটি পৃথক খারাপ জিনিস নিষিদ্ধ করা হচ্ছেঃ একটি আংশিক কার্যকরকরণ যা এমন একটি অবস্থায় পৌঁছায় যেখানে উত্তরটি এখনও তৈরি করা হয়নি এবং ঘড়ির মান (একটি অবস্থা পরিবর্তনশীল) সীমা লঙ্ঘন করে। ডেডলক স্বাধীনতা একটি নিরাপত্তা সম্পত্তিঃ "খারাপ জিনিস" একটি অচলাবস্থা (যা বিচ্ছিন্ন)। বেশিরভাগ সময়, একটি প্রোগ্রাম শেষ পর্যন্ত কিছু "ভাল কাজ" করে তা জানা সন্তোষজনক নয়; আমরা জানতে চাই যে প্রোগ্রামটি কিছু সংখ্যক ধাপের মধ্যে বা কিছু সময়সীমা আগে "ভাল কাজ" করে। একটি সম্পত্তি যা "ভাল জিনিস" কে একটি নির্দিষ্ট সীমা দেয় তা হল একটি নিরাপত্তা সম্পত্তি (উপরে উল্লিখিত হিসাবে), যেখানে দুর্বল সম্পত্তি যা কেবল সীমাবদ্ধতার অস্তিত্বকে দাবি করে তা হল একটি জীবন্ত সম্পত্তি। এই ধরনের প্রাণবন্ত সম্পত্তি প্রমাণ করা কঠিন নিরাপত্তা সম্পত্তি প্রমাণ করার চেয়ে সহজ হতে পারে কারণ প্রাণবন্ত সম্পত্তি প্রমাণ করার জন্য সুরক্ষা সম্পত্তি প্রমাণ করার জন্য প্রয়োজনীয় বিশদ অ্যাকাউন্টিংয়ের প্রয়োজন হয় না। একটি নিরাপত্তা সম্পত্তি থেকে আলাদা করার জন্য, একটি লাইভনেস সম্পত্তি একটি কার্যকরকরণের কোনও সীমাবদ্ধ উপসর্গকে বাতিল করতে পারে না (যেহেতু এই ধরনের একটি "খারাপ জিনিস" হবে এবং এইভাবে, একটি নিরাপত্তা সম্পত্তি সংজ্ঞায়িত করা হবে)। এটি একটি জীবন্ত বৈশিষ্ট্যকে এমন একটি বৈশিষ্ট্য হিসাবে সংজ্ঞায়িত করে যা কোনও সীমাবদ্ধ উপসর্গকে বাতিল করে না। এই সংজ্ঞাটি কোনও ভাল জিনিসকে বিচ্ছিন্ন হওয়ার মধ্যে সীমাবদ্ধ করে না-ভাল জিনিসটি সমস্ত কিছুকে জড়িত করতে পারে, যা একটি অসীম দৈর্ঘ্যের কার্যকরকরণ। হিস্ট্রি ল্যাম্পোর্ট তার 1977 সালের গবেষণাপত্রে মাল্টিপ্রোসেস (সমবর্তী) প্রোগ্রামগুলির সঠিকতা প্রমাণ করার জন্য সুরক্ষা সম্পত্তি এবং প্রাণবন্ত সম্পত্তি শব্দগুলি ব্যবহার করেছিলেন। তিনি পেট্রি নেট তত্ত্ব থেকে শব্দগুলি ধার করেছিলেন, যা একটি পেট্রি নেটের "টোকেন" এর "স্থান"-এর বরাদ্দ কীভাবে বিকশিত হতে পারে তা বর্ণনা করার জন্য জীবন্ততা এবং সীমানা শব্দগুলি ব্যবহার করছিল; পেট্রি নেট নিরাপত্তা ছিল সীমাবদ্ধতার একটি নির্দিষ্ট রূপ। ল্যাম্পোর্ট পরবর্তীকালে মিউনিখে ডিস্ট্রিবিউটেড সিস্টেমের উপর একটি ন্যাটো সংক্ষিপ্ত কোর্সের জন্য সুরক্ষার একটি আনুষ্ঠানিক সংজ্ঞা তৈরি করেছিলেন। এটি ধরে নিয়েছিল যে নড়াচড়ার অধীনে বৈশিষ্ট্যগুলি অপরিবর্তনীয়। উপরে প্রদত্ত সুরক্ষার আনুষ্ঠানিক সংজ্ঞাটি আলপার্ন এবং স্নাইডারের একটি গবেষণাপত্রে প্রকাশিত হয়েছে; আলপার্ন, ডেমার্স এবং স্নাইডারের একটি গবেষণাপত্রে সুরক্ষা বৈশিষ্ট্যের দুটি আনুষ্ঠানিকতার মধ্যে সংযোগটি প্রকাশিত হয়েছে। আলপার্ন এবং স্নাইডার জীবের আনুষ্ঠানিক সংজ্ঞা দিয়েছেন, একটি প্রমাণ সহ যে সমস্ত বৈশিষ্ট্য সুরক্ষা বৈশিষ্ট্য এবং জীবের বৈশিষ্ট্য ব্যবহার করে নির্মাণ করা যেতে পারে। এই প্রমাণটি গর্ডন প্লটকিনের অন্তর্দৃষ্টি দ্বারা অনুপ্রাণিত হয়েছিল যে নিরাপত্তা বৈশিষ্ট্যগুলি বদ্ধ সেটের সাথে মিলে যায় এবং জীবন্ত বৈশিষ্ট্যগুলি প্রোগ্রাম অবস্থার অসীম ক্রমের সেটের প্রাকৃতিক টপোলজিতে ঘন সেটের সাথে মিলে যায়। পরবর্তীকালে, আলপার্ন এবং স্নাইডার শুধুমাত্র সুরক্ষা বৈশিষ্ট্য এবং প্রাণবন্ত বৈশিষ্ট্যের আনুষ্ঠানিক সংজ্ঞার জন্য একটি বুচি অটোমেটন চরিত্রায়নই দেননি, বরং এই স্বয়ংক্রিয় সূত্রগুলি ব্যবহার করে দেখিয়েছেন যে সুরক্ষা বৈশিষ্ট্যগুলির যাচাইয়ের জন্য একটি অপরিবর্তনীয় এবং প্রাণবন্ত বৈশিষ্ট্যগুলির যাচাইকরণের জন্য একটি সুপ্রতিষ্ঠিত যুক্তি প্রয়োজন হবে। সম্পত্তির প্রকারের (নিরাপত্তা বনাম জীবন্ততা) সঙ্গে প্রমাণের প্রকারের (অপরিবর্তনীয় বনাম সুপ্রতিষ্ঠিততা) মধ্যে যোগাযোগ একটি শক্তিশালী যুক্তি ছিল যে সুরক্ষা এবং জীবন্ততায় বৈশিষ্ট্যগুলির পচন (অন্য কোনও বিভাজনের বিপরীতে) একটি দরকারী ছিল-সম্পত্তির প্রকারটি জানা যা প্রমাণিত হওয়ার জন্য প্রয়োজনীয় প্রমাণের ধরন নির্ধারণ করে। রেফারেন্স সমবর্তী কম্পিউটিং তাত্ত্বিক কম্পিউটার বিজ্ঞান মডেল চেকিং