فرامنطق‌های زمانی و راستی‌آزمایی برای فراویژگی‌ها
مهران سلیمان فلاح (دانشگاه صنعتی امیرکبیر)

چکیده
به شکل ترادادی، توصیف سامانه‌های رایانشی بیشتر با بیان خواسته‌ها از نشان‌های اجرای سامانه‌ها که به ویژگی‌های نشان نیز شناخته می‌شوند، انجام شده است. برای این کار، پژوهشگران از منطق‌های زمانی مانند اِلتیاِل و سیتیاِل و نیز گسترش‌های آنها بسیار بهره برده و ویژگی‌های نشان را بیان کرده‌اند. همچنین، دانشوران روش‌های گوناگونی برای راستی‌آزمایی سامانه‌ها برای این ویژگی‌ها پیشنهاد داده‌اند. با وجود این، آنچه از سامانه‌ها خواسته می‌شود، همگی با بیان ویژگی‌های تک‌نشان‌ها شدنی نیست. خواسته‌هایی مانند چونی زاوَری و نیز خواسته‌های وابسته به امنیت، از این نمونه‌ها هستند. از این روی، گونه‌ای دیگر از ویژگی‌های سامانه‌ها پیشنهاد شده‌اند که به جای تک‌نشان‌ها خواسته‌ای از گردایۀ همۀ نشان‌های اجرای سامانه بیان می‌کنند. به این خواسته‌ها فراویژگی می‌گویند و برای بیان آنها فرامنطق‌های زمانی را پیشنهاد داده‌اند. در این گفتار، بر آنم که به فراویژگی‌ها و منطق فرااِلتیاِل که یکی از فرامنطق‌های زمانی است، بپردازم. همچنین، برخی شیوه‌های راستی‌آزمایی سامانه‌ها برای فراویژگی‌ها مانند راستی‌آزمایی زمان‌اجرا و تفسیر انتزاعی را برای این دست از خواسته‌ها بیان کرده و چالش‌ها را در هم‌سنجی با راستی‌آزمایی برای ویژگی‌ها به گفتگو بگذارم.

تاریخ: دوشنبه، ۳۱ شهریور ۱۴۰۴، ساعت ۱۶ الی ۱۸
سخنرانی به صورت حضوری و مجازی به ميزبانی دانشگاه امیرکبیر

(تهران، خيابان حافظ، درب زير پل حافظ، دانشگاه صنعتی امیر کبیر، دانشکده ریاضی و علوم کامپیوتر، گروه ریاضی محض، اتاق ۳۱۱) برگزار می‌شود.

پیوند سخنرانی برخط (آنلاین)
https://meet.google.com/cpj-mhhf-kyc