Search

Your search keyword '"Simone, Robert"' showing total 3 results
Start Over Author "Simone, Robert" Publication Year Range Last 3 years Language english
3 results on '"Simone, Robert"'

1. Sémantique formelle du langage PsyC

Author

Siron, Fabien, Potop-Butucaru, Dumitru, de Simone, Robert, Chabrol, Damien, Methni, Amira, Logical Time for Formal Embedded System Design (KAIROS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), KRONO‐SAFE, and Inria - Sophia Antipolis

Subjects
Logical Execution Time, Système Temps-Réel, Multiform Logical Time, Sémantique Formelle, Temps d’Exécution Logique, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Real-Time Systems, Temps Logique Multiforme, Formal Semantics
Abstract

Time must be taken into account from the very start of the design of real-time systems. Because exact computation durations are usually not available in early design phase, multiple formalisms based on the concept of Multiform Logical Time have been introduced. Thesynchronous approach introduced a discretized abstraction of time based on logical clocks, on which computation happens logically instantaneously. While being very expressive, the synchronous approach suffer from compilation issues when mapping logical time to non-negligible real-time computation durations. In answer, the Logical Execution Time (LET) paradigm has been introduced to give such a compromise between the strong expressiveness of the synchronous approach and traditional task scheduling, making LET a perfect fit for the temporal architecture and the software integration of real-time systems. In this report, we consider a variation of LET extended with logical clocks, namely synchronous LET (sLET), implemented in the industrial language PsyC. The sLET approach — and thus PsyC — allows to specify computation to be executed inside a logical interval up to the next occurrence of a logical clock expression (i.e. in opposition to a constant duration). As sLET is based on both LET and the synchronous approach, we give in this report two operational semantics of the PsyC language: a native semantics (or big-step) based on the Structural Operational Semantics approach (S.O.S.) and a synchronous semantics defined by translation to the Esterel language. The former gathers all valid computation schedulings as an equivalence class, of which the latter provides a specific representative (as-soon-as-possible execution). We show the semantics equivalence of those two semantics at interval boundaries. While the native semantics is mainly used for compilation, future work will show how logical timing properties can be verified using those two semantics.; Le temps doit être pris en compte dès le début de la conception des systèmes temps-réel. Du fait que les durées exactes des calculs ne sont généralement pas disponibles au début de la phase de conception, plusieurs formalismes basés sur le concept de Temps Logique Multiforme ont été introduits dans la littérature. L’approche synchrone introduit une abstraction discrète du temps basée sur des horloges logiques, sur lesquels les calculs s’effectuent logiquement instantanément. Bien que très expressive, l’approche synchrone souffre de difficultés de compilation lors de l’association du temps logique à des durées de calculs non négligeables. En réponse, le paradigme Temps d’Exécution Logique (LET) a été introduit comme compromis entre l’expressivité de l’approche synchrone et l’ordonnancement temps-réel traditionnel, ce qui fait que le LET est parfaitement adapté à la modélisation d’architecture temporelle. Dans ce rapport, nous considérons une variation du LET enrichi via l’usage d’horloges logiques, que nous appellerons LET synchrone (sLET), implémenté par le langage industriel PsyC. L’approche sLET— et donc le PsyC — permet de spécifier un calcul comme étant exécuté au sein d’un intervalle de temps logique jusqu’à la prochaine occurrence d’une expression d’horloge (en opposition à une durée constante). Du fait que sLET est basé à la fois sur LET et sur l’approche synchrone, nous donnons dans ce rapport deux sémantiques opérationnelles du PsyC : une sémantique native (ou grand pas) basée sur une approche à la Plotkin (S.O.S.) et une sémantique synchrone définie par traduction vers le langage Esterel. La première regroupe tous les ordonnancement valides sous forme de classe d’équivalence, dans laquelle la seconde donne un représentant spécifique (dès que possible). Nous montrons l’équivalence sémantique de ces deux sémantiques sur les bornes des intervalles. La sémantique native est principalement utilisée pour la compilation, tandis que des travaux à venir montreront comment vérifier des propriétés de temporisation en utilisant essentiellement la sémantique synchrone.

Published
2023

2. The synchronous Logical Execution Time paradigm

Author

Siron, Fabien, Potop-Butucaru, Dumitru, de Simone, Robert, Chabrol, Damien, Methni, Amira, KRONO‐SAFE, Université Côte d'Azur (UCA), Logical Time for Formal Embedded System Design (KAIROS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), and COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)

Subjects
[INFO.INFO-ES]Computer Science [cs]/Embedded Systems, ComputingMilieux_MISCELLANEOUS
Abstract

International audience; Real-Time industrial systems are not so much of those that have to perform tasks incredibly fast, but in a timepredictable manner; they rather focus on meeting previously specified timing requirements in a provable way. Consequently, time must be taken into account from the very start of the design. However, exact timing constants may not be available yet inearly design stages as they may depend on the target. In answer, formalisms based on the Multiform Logical Time have been introduced to abstract real-time durations. The Synchronous-Reactive (SR) approach introduced a discretized abstraction of time on which computations happen logically instantaneously. Contrary to SR, Logical Execution Time (LET) mandates to specify the actual logical duration a task has to fulfill. This allows a more efficient compilation, at the price of a lower expressiveness. Classical LET (i.e. as introduced in Giotto/TDL) sticks to uniform pseudo-physical time, i.e. based on one logical clock mapped to the real-time. In this paper, we introduce a new paradigm called synchronous Logical Execution Time (sLET) that builds upon both SR and LET paradigms. It keeps the idea of logical durations coming from the LET paradigm, while having logical instants based on logical clocks. This extends the expressivity of LET, as time is totally abstracted as sequences of events. The various schedulings provide physically timedversions that, while having distinct non-functional properties (in terms of performance mostly), remain mutually functionally equivalent (in the logical time realm). A particular instance, where computations are executed ”in a single instant”, and then time is advanced (as in classical event-driven simulation), can lead to a direct translation into synchronous formalisms (in our case Esterel). We started inquiring how this could open new ways of verification and analysis on PsyC program.

Published
2022

3. Contributors

Author

Abdel-Wahab, Omar, Abrahm, Janet L., Abutalib, Syed A., Adams, Sharon, Al Hadidi, Samer, Alcaide, Pilar, Allen, Carl E., Ambinder, Richard F., Amonoo, Hermioni L., Anderson, Julia A.M., Antin, Joseph H., Antony, Aśok C., Araten, David J., Arnold, Donald M., Awan, Farrukh T., Ayers, Emily C., Barth, Peter, Bates, Shannon M., Benz, Edward J., Berliner, Nancy, Bhardwaj, Nina, Bhatia, Smita, Bhatt, Mihir D., Bollard, Catherine M., Bowman, Mackenzie, Boyle, Eileen M., Braun, Benjamin S., Brenner, Malcolm K., Broccoli, Alessandro, Brodsky, Robert A., Brown, Myles, Broxmeyer, Hal E., Brummel-Ziedins, Kathleen, Brunner, Andrew M., Brunstein, Claudio G., Buadi, Francis K., Burkhardt, Birgit, Burns, Melissa A., Bussel, James B., Byrd, John C., Caimi, Paolo F., Camaschella, Clara, Canavan, Michelle, Cantor, Alan B., Capitano, Maegan L., Carcao, Manuel, Carrillo-Farga, Joaquin, Carroll, Michael C., Carson, William E., Carty, Shannon A., Castillo, Jorge J., Chakrabarti, Priyasmita, Chan, Anthony K.C., Chan, Noel C., Chhabra, Saurabh, Chute, John P., Cimen Bozkus, Cansu, Ciurea, Stefan O., Coates, Thomas D., Collins, Graham, Creager, Mark A., Cromwell, Caroline, Crowder, Lauren A., Cushing, Melissa M., Cutler, Corey, Dabaja, Bouthaina, Dave, Sandeep S., De, Caprio, James A., De, Carli, Kathryn, Deininger, Michael W., De, Simone, Robert A., Dinauer, Mary C., Dinner, Shira, Dixit, Karan S., Dogan, Ahmet, Dorshkind, Kenneth, Dotti, Gianpietro, Dror, Yigal, Dunleavy, Kieron, Dvorak, Christopher C., Ebert, Benjamin L., Eck, Michael J., Eckstein, Olive S., Eikelboom, John W., El Jamal, Siraj M., El-Jurdi, Najla, Kim El-Mallawany, Nader, Erba, Harry P., Evans, William E., Feld, Jonathan, Feldman, Alexander, Ferrara, James L., Fischer, Martin, Forbes, Lisa R., Franco, Idalid, Fredenburgh, James C., Frey, Noelle V., Friedman, Kenneth D., Fuller, Stephen J., Gabe, Caroline, Gailani, David, Gallagher, Patrick G., Gallardo-Grajeda, Andrea, Ganz, Tomas, Gee, Adrian P., George, Gemlyn, Gerson, Stanton L., Gertz, Morie A., Ghosh, Nilanjan, Gibson, Christopher J., Ginzburg, Yelena Z., Gomez, Keith, Gotlib, Jason, Grant, Shakira J., Graubert, Timothy A., Gregg, Xylina T., Gribben, John G., Gross, Peter L., Gulati, Nitya, Gurbuxani, Sandeep, Gutierrez, Alejandro, de Haan, Gerald, Haas-Kogan, Daphne, Haddad, Montaser, Halene, Stephanie, Hamadani, Mehdi, Hammond, Rebecca M., Hari, Parameswaran N., Hayman, Suzanne R., Hayward, Catherine, Hebbel, Robert P., Heidenreich, Olaf, Henkin, Stanislav, Hensch, Lisa, Hillis, Christopher, Hillyer, Christopher D., Hoffman, Ronald, Horny, Hans-Peter, Horowitz, Mia, Hsu, Katharine, Hub, Elin, Iancu-Rubin, Camelia, Isenman, David E., Israels, Sara J., Italiano, Joseph E., Jaffe, Elaine S., Jaffer, Iqbal H., Jäger, Ulrich, Jain, Nitin, James, Paula, Jimenez, Alexandra, Jordan, Michael B., Jung, Moonjung, Kager, Leo, Kanakry, Jennifer A., Kanate, Abraham S., Kelly, Kara M., Khandoga, Alexander G., Karsan, Aly, Kaufman, Richard M., Keyzner, Alla, Khanna-Gupta, Arati, Kharchenko, Evgeniya, Klein, Harvey G., Klepin, Heidi D., Anders Kolb, E., Kollet, Orit, Konopleva, Marina, Kontoyiannis, Dimitrios P., Koreth, John, Koretzky, Gary A., Kozieł-Siołkowska, Monika, Kremyanskaya, Marina, Kucine, Nicole, Kumar, Shaji, Küppers, Ralf, Lacy, Martha Q., Ola Landgren, C., Landier, Wendy, Lane, Andrew A., Lane, William J., Langer, Arielle L., Lapidot, Tsvee, Laureano, Marissa, Leblanc, Francis R., Le, Blanc, Thomas W., La, Casce, Ann S., Lee, Daniel W., Lee, Kathleen A., Leung, Wingchi, Levi, Marcel, Lewis, Russell E., Lichtman, Eben I., Lin, Judith C., Lin, Richard J., Lip, Gregory, Poh Loh, Kah, López, José A., Zoref Lorenz, Adi, Loughran, Thomas P., Lu, Sydney X., Lukas, Rimas V., Lulla, Premal, Luscinskas, Francis W., Ma, Alice D., Maakaron, Joseph E., Machlus, Kellie R., Maciejewski, Jaroslaw P., Magenau, John, Majhail, Navneet, Malek, Ehsan, Manis, John P., Mann, Kenneth G., Manno, Catherine S., Marcellino, Bridget K., Marcogliese, Andrea N., Marincola, Francesco M., Mascarenhas, John, Massberg, Steffen, Matino, Davide, Mc, Ever, Rodger P., Mc, Grath, Emer, Mc, Guire, Hilary, S. Mc, Kinney, Matthew, Mehta, Atul, A. Menapace, Laurel, Mentzer, William C., Michel, Marc, Rita Migliaccio, Anna, Mims, Martha P., Moffat, Karen A., Morgan, Gareth J., Najfeld, Vesna, Naymagon, Leonard, Ness, Paul M., Ng, Andrea K., Ning, Shuoyan, Notarangelo, Luigi D., O'Donnell, Martin, Ollila, Thomas A., Ordonez-Moreno, Alejandra, Own, Maryam, Pai, Menaka, Pai, Sung-Yun, Paidas, Michael, Papa, Luena, Papayannopoulou, Thalia, Peng, Cynthia S., Wang Petersdorf, Effie, Pickard, Lucy, Pierce, Glenn F., Pittaluga, Stefania, Porteus, Matthew, Potpara, Tatjana S., Prchal, Josef T., Puigserver, Pere, Vincent Rajkumar, S., Rak, Janusz, Ramos, Carlos A., Rand, Jacob H., Rand, Margaret L., Rao, Dinesh S., Rappazzo, Katherine C., Rau, Rachel E., Ravandi, Farhad, Rawley, Orla, Rawlings, David J., Reddy, Pavan, Reiter, Andreas, Reville, Barbara, Rice, Lawrence, Riese, Matthew J., Rippel, Noa, Riwes, Mary, Roberts, David J., Rodrigue, Bentley B., Rojek, Alexandra E., Roman, Elizabeth, Rossmann, Marlies P., Rot, Antal, Rouce, Rayne H., Rowley, Scott D., Rustad, Even H., Sahni, Gagan, Sahoo, Daisy, Salama, Mohamed E., Samji, Nasrin, Scadden, David, Schiffman, Fred J., Schipperus, Martin R., Schrier, Stanley L., Shaz, Beth H., Shelburne, Samuel A., Sheth, Sujit, Sholevar, Roxanne, Silberstein, Lev, Silverman, Lewis B., Silverstein, Roy L., Skeith, Leslie, Sloan, Steven R., Douglas Smith, Stephen, Steensma, David P., Steinberg, Martin H., Stieglitz, Elliot, Stock, Wendy, Storry, Jill R., Stramer, Susan L., Strati, Paolo, Stroncek, David F., Flohr Svendsen, Arthur, Sweetenham, John W., Tebaldi, Toma, Teegavarapu, Sravanti P., Tewari, Alok, Lay Thein, Swee, Tillman, Benjamin F., Tomlinson, Benjamin, Tremblay, Douglas, Treon, Steven P., Tsai, Frederick D., Tsang, Mazie, Tzannou, Ifigeneia, Usmani, Saad Z., Valent, Peter, Venkataraman, Girish, Venugopal, Sangeetha, M. Vercellotti, Gregory, Viero, Gabriella, von Andrian, Ulrich H., Vose, Julie M., Wagner, Andrew J., Wang, Ena, Wang, Jia-huai, Warkentin, Theodore E., Weitz, Jeffrey I., West, Kamille A., Westhoff, Connie M., Wheeler, Allison P., Wierda, William, Wiersum-Osselton, Johanna C., Wiley, James S., Williams, David A., Wolgast, Lucia R., Yang, Daozheng, Yang, Moua, Younes, Anas, Young, Neal S., Zayac, Adam S., Zeller, Michelle P., Zieske, Arthur W., Zimran, Ari, Luigi Zinzani, Pier, C. Zubair, Abba, and Michel Zwaan, C.

Published
2023
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results